:: The Formalisation of Simple Graphs :: by Yozo Toda :: :: Received September 8, 1994 :: Copyright (c) 1994-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FINSEQ_1, XXREAL_0, CARD_1, XBOOLE_0, ARYTM_3, TARSKI, FINSET_1, ZFMISC_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSUB_1, SETWISEO, MCART_1, RELAT_1, ORDINAL4, SGRAPH1, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, XTUPLE_0, MCART_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, FINSEQ_2, FINSUB_1, SETWISEO, XXREAL_0; constructors WELLORD2, SETWISEO, NAT_1, FINSEQ_2, STRUCT_0, XTUPLE_0, NUMBERS; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XXREAL_0, NAT_1, FINSEQ_1, CARD_1, XTUPLE_0, XCMPLX_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI; equalities FINSEQ_1; expansions TARSKI; theorems TARSKI, ENUMSET1, ZFMISC_1, NAT_1, FINSEQ_1, FINSEQ_3, FINSUB_1, CARD_1, CARD_2, FINSET_1, XBOOLE_0, XBOOLE_1, XXREAL_0; schemes SETWISEO, XFAMILY; begin :: interval is defined as subset of reals in measure5. :: so we use a symbol nat_interval here. :: following the definition of Seg, I add an assumption 1 <= m. :: but it is unnatural, I think. :: I changed the proof of existence :: so that the assumption (1 <= m) is not necessary. :: now nat_interval has the very natural definition, I think (-: definition let m,n be Nat; func nat_interval(m,n) -> Subset of NAT equals {i where i is Nat: m<=i & i<=n}; coherence proof set IT = {i where i is Nat : m<=i & i<=n}; now let e be object; assume e in IT; then consider i being Nat such that A1: i=e and m<=i and A2: i<=n; now per cases; suppose i=0; then i in {0} by TARSKI:def 1; hence e in ({0}\/(Seg n)) by A1,XBOOLE_0:def 3; end; suppose i<>0; then (0+1)<=i by NAT_1:13; then e in (Seg n) by A1,A2; hence e in ({0} \/ (Seg n)) by XBOOLE_0:def 3; end; end; hence e in ({0} \/ (Seg n)); end; then A3: IT c= ({0} \/ (Seg n)); {0} c= NAT by ZFMISC_1:31; then {0}\/(Seg n) c= NAT by XBOOLE_1:8; hence thesis by A3,XBOOLE_1:1; end; end; notation let m,n be Nat; synonym Seg (m,n) for nat_interval (m,n); end; registration let m,n be Nat; cluster nat_interval(m,n) -> finite; coherence proof set IT = {i where i is Nat : m<=i & i<=n}; now let e be object; assume e in IT; then consider i being Nat such that A1: i=e and m<=i and A2: i<=n; now per cases; suppose i=0; then i in {0} by TARSKI:def 1; hence e in ({0}\/(Seg n)) by A1,XBOOLE_0:def 3; end; suppose i<>0; then (0+1)<=i by NAT_1:13; then e in (Seg n) by A1,A2; hence e in ({0} \/ (Seg n)) by XBOOLE_0:def 3; end; end; hence e in ({0} \/ (Seg n)); end; then IT c= {0} \/ Seg n; hence thesis; end; end; theorem for m,n being Nat, e being set holds e in nat_interval(m,n) iff ex i being Nat st e=i & m<=i & i<=n; theorem for m,n,k being Nat holds k in nat_interval(m,n) iff m<=k & k<=n proof let m,n,k be Nat; hereby assume k in nat_interval(m,n); then ex i being Nat st k=i & m<=i & i<=n; hence m<=k & k<=n; end; assume m <= k & k <= n; hence thesis; end; theorem for n being Nat holds nat_interval (1,n) = Seg n; theorem Th4: for m,n being Nat st 1 <= m holds nat_interval(m,n) c= Seg n proof let m,n be Nat; assume A1: 1<=m; now let e be object; assume e in nat_interval(m,n); then consider i being Nat such that A2: e=i and A3: m<=i and A4: i<=n; 1<=i by A1,A3,XXREAL_0:2; hence e in Seg n by A2,A4; end; hence thesis; end; theorem Th5: for k,m,n being Nat st k set equals {z where z is finite Subset of A : card z = 2}; coherence; end; theorem Th7: for A be set, e be set holds (e in TWOELEMENTSETS(A) iff ex z being finite Subset of A st e = z & (card z)=2 ); theorem Th8: for A be set, e be set holds (e in TWOELEMENTSETS(A) iff (e is finite Subset of A & ex x,y being object st x in A & y in A & x<>y & e = {x,y} )) proof let A be set, e be set; hereby assume e in TWOELEMENTSETS(A); then A1: ex z being finite Subset of A st e=z & (card z)=2; then reconsider e9=e as finite Subset of A; thus e is finite Subset of A by A1; consider x,y being object such that A2: x<>y and A3: e9={x,y} by A1,CARD_2:60; take x,y; x in e9 & y in e9 by A3,TARSKI:def 2; hence x in A & y in A; thus x<>y & e={x,y} by A2,A3; end; assume that e is finite Subset of A and A4: ex x,y being object st x in A & y in A & x<>y & e={x,y}; consider x,y being Element of A such that A5: x in A and y in A and A6: not x=y and A7: e={x,y} by A4; reconsider xy = {x,y} as finite Subset of A by A5,ZFMISC_1:32; ex z being finite Subset of A st e=z & (card z)=2 proof take xy; thus e=xy by A7; thus thesis by A6,CARD_2:57; end; hence thesis; end; theorem Th9: for A being set holds TWOELEMENTSETS(A) c= (bool A) proof let A be set; now let x be object; assume x in TWOELEMENTSETS(A); then x is finite Subset of A by Th8; hence x in (bool A); end; hence thesis; end; theorem Th10: for A being set, e1,e2 being set st {e1,e2} in TWOELEMENTSETS(A) holds e1 in A & e2 in A & e1<>e2 proof let A be set, e1,e2 be set; assume A1: {e1,e2} in TWOELEMENTSETS(A); then consider x,y being object such that A2: x in A & y in A & not x=y and A3: {e1,e2} = {x,y} by Th8; per cases by A3,ZFMISC_1:6; suppose e1=x & e2=x; then {x} in TWOELEMENTSETS(A) by A1,ENUMSET1:29; then ex x1,x2 being object st x1 in A & x2 in A &( not x1=x2)& { x} = {x1,x2} by Th8; hence thesis by ZFMISC_1:5; end; suppose e1=x & e2=y; hence thesis by A2; end; suppose e1=y & e2=x; hence thesis by A2; end; suppose e1=y & e2=y; then {y} in TWOELEMENTSETS(A) by A1,ENUMSET1:29; then ex x1,x2 being object st x1 in A & x2 in A &( not x1=x2)& { y}={x1,x2} by Th8; hence thesis by ZFMISC_1:5; end; end; theorem Th11: TWOELEMENTSETS {} = {} proof TWOELEMENTSETS {} c= {} proof let a be object; assume a in TWOELEMENTSETS({}); then ex a1,a2 being object st a1 in {} & a2 in {} &( not a1=a2)& a = {a1,a2} by Th8; hence thesis; end; hence thesis; end; theorem for t,u being set st t c= u holds TWOELEMENTSETS(t) c= TWOELEMENTSETS( u) proof let t,u be set; assume A1: t c= u; let e be object; assume A2: e in TWOELEMENTSETS(t); then e is finite Subset of t by Th8; then A3: e is finite Subset of u by A1,XBOOLE_1:1; ex x,y being object st x in t & y in t &( not x=y)& e={x,y} by A2,Th8; hence thesis by A1,A3,Th8; end; theorem Th13: for A being finite set holds TWOELEMENTSETS(A) is finite by Th9,FINSET_1:1; theorem for A being non trivial set holds TWOELEMENTSETS(A) is non empty proof let A be non trivial set; consider a being object such that A1: a in A by XBOOLE_0:def 1; reconsider A9 = A as non empty non trivial set; (A9\{a}) is non empty set by ZFMISC_1:139; then consider b being object such that A2: b in (A9\{a}) by XBOOLE_0:def 1; not b in {a} by A2,XBOOLE_0:def 5; then A3: a<>b by TARSKI:def 1; {a,b} c= A by A1,A2,ZFMISC_1:32; hence thesis by A1,A2,A3,Th8; end; theorem for a being set holds TWOELEMENTSETS {a} = {} proof let a be set; now let x be object; assume x in TWOELEMENTSETS({a}); then consider u,v being object such that A1: u in {a} and A2: v in {a} and A3: u<>v and x = {u,v} by Th8; u = a by A1,TARSKI:def 1 .= v by A2,TARSKI:def 1; hence contradiction by A3; end; hence thesis by XBOOLE_0:def 1; end; reserve X for set; begin :: SECTION 1: SIMPLEGRAPHS. :: graph is defined as a pair of two sets, of vertices and of edges. :: we treat only simple graphs; :: edges are non-directed, there is no loop, :: between two vertices is at most one edge. :: we define the set of all graphs SIMPLEGRAPHS, :: and later define some operations on graphs :: (contraction, deletion, minor, etc.) as relations on SIMPLEGRAPHS. :: Vertices and Edges are used in graph_1. so we must use different names. :: we restrict simple graphs as finite ones :: to treat degree as a cardinal of a set of edges. definition struct (1-sorted) SimpleGraphStruct (# carrier -> set, SEdges -> Subset of TWOELEMENTSETS(the carrier) #); end; :: SIMPLEGRAPHS is the set of all (simple) graphs, :: which is the smallest set satisfying following three conditions: :: (1) it contains , :: (2) if is an element of SIMPLEGRAPHS and n is not a vertex of , :: then <(V U {n}),E> is also an element of SIMPLEGRAPHS, :: (3) if is an element of SIMPLEGRAPHS, :: v1,v2 are different vertices of , :: and {v1,v2} is not an edge of , :: then is also an element of SIMPLEGRAPHS. definition let X be set; func SIMPLEGRAPHS(X) -> set equals the set of all SimpleGraphStruct (# v,e #) where v is finite Subset of X, e is finite Subset of TWOELEMENTSETS(v) ; coherence; end; theorem Th16: SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) in SIMPLEGRAPHS(X) proof reconsider phiv = {} as finite Subset of X by XBOOLE_1:2; reconsider phie = {}TWOELEMENTSETS{} as finite Subset of TWOELEMENTSETS(phiv ); SimpleGraphStruct (#phiv,phie#) in the set of all SimpleGraphStruct (# v,e #) where v is finite Subset of X, e is finite Subset of TWOELEMENTSETS(v) ; hence thesis; end; registration let X be set; cluster SIMPLEGRAPHS(X) -> non empty; coherence by Th16; end; definition let X be set; mode SimpleGraph of X -> strict SimpleGraphStruct means :Def4: it is Element of SIMPLEGRAPHS(X); existence proof take SimpleGraphStruct (# {},{}TWOELEMENTSETS{} #); thus thesis by Th16; end; end; theorem Th17: for g being object holds (g in SIMPLEGRAPHS(X) iff ex v being finite Subset of X, e being finite Subset of TWOELEMENTSETS(v) st g = SimpleGraphStruct (#v,e#)); begin :: SECTION 2: destructors for SimpleGraphStruct. theorem Th18: for g being SimpleGraph of X holds (the carrier of g) c= X & ( the SEdges of g) c= TWOELEMENTSETS (the carrier of g) proof let g be SimpleGraph of X; g is Element of SIMPLEGRAPHS(X) by Def4; then ex v being finite Subset of X, e being finite Subset of TWOELEMENTSETS(v) st g = SimpleGraphStruct (#v,e#) by Th17; hence (the carrier of g) c= X; thus thesis; end; theorem for g being SimpleGraph of X, e being set st e in the SEdges of g ex v1,v2 being object st v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 & e={v1,v2} by Th8; theorem for g being SimpleGraph of X, v1,v2 being set st {v1,v2} in the SEdges of g holds v1 in (the carrier of g) & v2 in the carrier of g & v1 <> v2 by Th10 ; theorem Th21: for g being SimpleGraph of X holds (the carrier of g) is finite Subset of X & (the SEdges of g) is finite Subset of TWOELEMENTSETS(the carrier of g) proof let g be SimpleGraph of X; g is Element of SIMPLEGRAPHS(X) by Def4; then ex v being finite Subset of X, e being finite Subset of TWOELEMENTSETS(v) st g = SimpleGraphStruct (#v,e#) by Th17; hence thesis; end; :: SECTION 3: equality relation on SIMPLEGRAPHS. :: two graphs are said to be "isomorphic" if :: (1) there is bijective function (i.e. set-theoretic isomorphism) :: between two sets of vertices, :: (2) this iso. respects the correspondence of edges. definition let X; let G,G9 be SimpleGraph of X; pred G is_isomorphic_to G9 means ex Fv being Function of the carrier of G, the carrier of G9 st Fv is bijective & for v1,v2 being Element of G holds ({v1, v2} in (the SEdges of G) iff {Fv.v1, Fv.v2} in the SEdges of G); end; begin :: SECTION 4: properties of SIMPLEGRAPHS. :: here is the induction principle on SIMPLEGRAPHS(X). scheme IndSimpleGraphs0 { X()-> set, P[set] } : for G being set st G in SIMPLEGRAPHS(X()) holds P[G] provided A1: P[SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#)] and A2: for g being SimpleGraph of X(), v being set st g in SIMPLEGRAPHS(X() ) & P[g] & v in X() & not v in (the carrier of g) holds P[SimpleGraphStruct (#( the carrier of g)\/{v}, {}TWOELEMENTSETS((the carrier of g)\/{v})#)] and A3: for g being SimpleGraph of X(), e being set st P[g] & e in TWOELEMENTSETS(the carrier of g) & not e in (the SEdges of g) holds ex sege being Subset of TWOELEMENTSETS(the carrier of g) st sege=((the SEdges of g)\/{e }) & P[SimpleGraphStruct (#(the carrier of g),sege#)] proof let g be set; assume A4: g in SIMPLEGRAPHS(X()); then A5: ex v being finite Subset of X(), e being finite Subset of TWOELEMENTSETS( v) st g = SimpleGraphStruct (#v,e#); then reconsider G = g as SimpleGraph of X() by A4,Def4; A6: (the carrier of G) c= X() by Th18; per cases; suppose A7: X() is empty; then (the SEdges of G) is Subset of {} by A6,Th11; hence thesis by A1,A6,A7; end; suppose X() is not empty; then reconsider X = X() as non empty set; defpred X[set] means P[SimpleGraphStruct (#\$1,{}TWOELEMENTSETS(\$1)#)]; A8: now let B9 be (Element of Fin X), b be Element of X; set g= SimpleGraphStruct (#B9,{}TWOELEMENTSETS(B9)#); B9 is finite Subset of X by FINSUB_1:16; then A9: g in SIMPLEGRAPHS(X()); then reconsider g as SimpleGraph of X() by Def4; assume ( X[B9])& not b in B9; then P[SimpleGraphStruct (#(the carrier of g)\/{b}, {}TWOELEMENTSETS(( the carrier of g)\/{b})#)] by A2,A9; hence X[B9 \/ {b}]; end; A10: X[{}.X] by A1; A11: for VV being Element of Fin X holds X[VV] from SETWISEO:sch 2(A10,A8 ); A12: now let VV be Element of (Fin X); per cases; suppose A13: TWOELEMENTSETS(VV) = {}; let EEa be Element of Fin TWOELEMENTSETS(VV), EE be Subset of TWOELEMENTSETS(VV); assume EEa = EE; EE = {}TWOELEMENTSETS(VV) by A13; hence P[SimpleGraphStruct (#VV,EE#)] by A11; end; suppose TWOELEMENTSETS(VV) <> {}; then reconsider TT = TWOELEMENTSETS(VV) as non empty set; defpred Q[Element of Fin TT] means for EE being Subset of TWOELEMENTSETS(VV) st EE = \$1 holds P[SimpleGraphStruct (#VV,EE#)]; A14: now let ee be Element of Fin TT, vv be Element of TT such that A15: Q[ee] and A16: not vv in ee; reconsider ee9 = ee as Subset of TWOELEMENTSETS(VV) by FINSUB_1:16; set g = SimpleGraphStruct (#VV,ee9#); VV is finite Subset of X() by FINSUB_1:16; then g is Element of SIMPLEGRAPHS(X()) by Th17; then reconsider g as SimpleGraph of X() by Def4; P[g] by A15; then ex sege being Subset of TWOELEMENTSETS(the carrier of g) st sege =((the SEdges of g)\/{vv}) & P[SimpleGraphStruct (#(the carrier of g), sege#)] by A3,A16; hence Q[ee \/ {.vv.}]; end; A17: Q[{}.TT] proof let EE be Subset of TWOELEMENTSETS(VV); assume EE = {}.TT; then EE = {}TWOELEMENTSETS(VV); hence thesis by A11; end; for EE being Element of Fin TT holds Q[EE] from SETWISEO:sch 2( A17,A14); hence for EE being Element of Fin TWOELEMENTSETS(VV), EE9 being Subset of TWOELEMENTSETS(VV) st EE9 = EE holds P[SimpleGraphStruct (#VV,EE9#)]; end; end; (the carrier of G) is Element of Fin X & (the SEdges of G) is Element of Fin TWOELEMENTSETS(the carrier of G) by A5,FINSUB_1:def 5; hence thesis by A12; end; end; :: now we give a theorem characterising SIMPLEGRAPHS as :: an inductively defined set. we need some lemmas. theorem for g being SimpleGraph of X holds (g=SimpleGraphStruct (#{},{} TWOELEMENTSETS{}#) or ex v being set, e being Subset of TWOELEMENTSETS(v) st v is non empty & g=SimpleGraphStruct (#v,e#) ) proof let g be SimpleGraph of X; assume A1: not g=SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#); take (the carrier of g), (the SEdges of g); thus (the carrier of g) is non empty by A1,Th11; thus thesis; end; theorem Th23: for V being Subset of X, E being Subset of TWOELEMENTSETS(V), n being set, Evn being finite Subset of TWOELEMENTSETS(V \/ {n}) st SimpleGraphStruct (#V,E#) in SIMPLEGRAPHS(X) & n in X holds SimpleGraphStruct (#(V \/ {n}),Evn#) in SIMPLEGRAPHS(X) proof let V be Subset of X, E be Subset of TWOELEMENTSETS(V), n be set, Evn be finite Subset of TWOELEMENTSETS(V \/ {n}); set g = SimpleGraphStruct (#V,E#); assume that A1: g in SIMPLEGRAPHS(X) and A2: n in X; reconsider g as SimpleGraph of X by A1,Def4; V = (the carrier of g); then V is finite Subset of X by Th21; then (V \/ {n}) is finite Subset of X by A2,Lm1; hence thesis; end; theorem Th24: for V being Subset of X, E being Subset of TWOELEMENTSETS(V), v1 ,v2 being set st v1 in V & v2 in V & v1<>v2 & SimpleGraphStruct (#V,E#) in SIMPLEGRAPHS(X) holds ex v1v2 being finite Subset of TWOELEMENTSETS(V) st v1v2 = (E \/ {{v1,v2}}) & SimpleGraphStruct (#V,v1v2#) in SIMPLEGRAPHS(X) proof let V be Subset of X, E be Subset of TWOELEMENTSETS(V), v1,v2 be set; set g = SimpleGraphStruct (#V,E#); assume that A1: v1 in V & v2 in V and A2: not v1=v2 and A3: g in SIMPLEGRAPHS(X); reconsider g as SimpleGraph of X by A3,Def4; A4: (the SEdges of g) is finite Subset of TWOELEMENTSETS(V) by Th21; (the carrier of g) is finite Subset of X by Th21; then reconsider V as finite Subset of X; (E \/ {{v1,v2}}) c= TWOELEMENTSETS(V) & (E \/ {{v1,v2}}) is finite proof hereby let e be object; assume A5: e in E \/ {{v1,v2}}; per cases by A5,XBOOLE_0:def 3; suppose e in E; hence e in TWOELEMENTSETS(V); end; suppose e in {{v1,v2}}; then A6: e={v1,v2} by TARSKI:def 1; then e is Subset of V by A1,ZFMISC_1:32; hence e in TWOELEMENTSETS(V) by A1,A2,A6,Th8; end; end; thus thesis by A4; end; then reconsider E9 = (E \/ {{v1,v2}}) as finite Subset of TWOELEMENTSETS(V); SimpleGraphStruct (#V,E9#) in SIMPLEGRAPHS(X); hence thesis; end; :: next we define a predicate :: which describe how SIMPLEGRAPHS are generated inductively. :: *** QUESTION *** :: conditions (not n in V) and (not {v1,v2} in E) are redundant? definition let X be set, GG be set; pred GG is_SetOfSimpleGraphs_of X means SimpleGraphStruct (#{},{} TWOELEMENTSETS{}#) in GG & (for V being Subset of X, E being Subset of TWOELEMENTSETS(V), n being set, Evn being finite Subset of TWOELEMENTSETS(V \/ {n}) st (SimpleGraphStruct (#V,E#) in GG & n in X & not n in V) holds SimpleGraphStruct (#(V \/ {n}),Evn#) in GG) & for V being Subset of X, E being Subset of TWOELEMENTSETS(V), v1,v2 being set st SimpleGraphStruct (#V,E#) in GG & v1 in V & v2 in V & v1<>v2 & (not {v1,v2} in E) holds ex v1v2 being finite Subset of TWOELEMENTSETS(V) st v1v2 = (E \/ {{v1,v2}}) & SimpleGraphStruct (#V, v1v2#) in GG; end; theorem Th25: SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X by Th16,Th23,Th24; theorem Th26: for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds SIMPLEGRAPHS(X) c= OTHER proof let OTHER be set; defpred X[set] means \$1 in OTHER; assume A1: OTHER is_SetOfSimpleGraphs_of X; A2: for g being SimpleGraph of X, v being set st g in SIMPLEGRAPHS(X) & X[g] & v in X & not v in (the carrier of g) holds X[SimpleGraphStruct (#(the carrier of g)\/{v}, {}TWOELEMENTSETS((the carrier of g)\/{v})#)] proof let g be SimpleGraph of X, v be set; assume that g in SIMPLEGRAPHS(X) and A3: g in OTHER & v in X & not v in (the carrier of g); set SVg=(the carrier of g); SVg is Subset of X by Th21; hence thesis by A1,A3; end; A4: for g being SimpleGraph of X, e being set st X[g] & e in TWOELEMENTSETS( the carrier of g) & not e in (the SEdges of g) holds ex sege being Subset of TWOELEMENTSETS(the carrier of g) st sege=((the SEdges of g)\/{e}) & X[ SimpleGraphStruct (#(the carrier of g),sege#)] proof let g be SimpleGraph of X, e be set; assume that A5: g in OTHER and A6: e in TWOELEMENTSETS(the carrier of g) and A7: not e in (the SEdges of g); set SVg = (the carrier of g), SEg = (the SEdges of g); consider v1,v2 being object such that A8: v1 in SVg & v2 in SVg & v1<>v2 and A9: e={v1,v2} by A6,Th8; SVg is finite Subset of X by Th21; then consider v1v2 being finite Subset of TWOELEMENTSETS(SVg) such that A10: v1v2=(SEg \/ {{v1,v2}}) & SimpleGraphStruct (#SVg,v1v2#) in OTHER by A1,A5,A7,A8,A9; take v1v2; thus thesis by A9,A10; end; let e be object; assume A11: e in SIMPLEGRAPHS(X); A12: X[SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#)] by A1; for e being set st e in SIMPLEGRAPHS(X) holds X[e] from IndSimpleGraphs0(A12,A2,A4); hence thesis by A11; end; theorem SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X & for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds SIMPLEGRAPHS(X) c= OTHER by Th25,Th26; begin :: SECTION 5: SubGraphs. :: graph G is a subgraph of graph G' if :: (1) the set of vertices of G is a subset of the set of vertices of G', :: (2) the set of edges of G is a subset of the set of edges of G', :: where two endpoints of each edge of G must be the vertices of G. :: (of course G must be a graph!) :: now no lemma is proved )-: definition let X be set, G be SimpleGraph of X; mode SubGraph of G -> SimpleGraph of X means the carrier of it c= the carrier of G & the SEdges of it c= the SEdges of G; existence; end; begin :: SECTION 6: degree of vertices. :: the degree of a vertex means the number of edges connected to that vertex. :: in the case of simple graphs, we can prove that :: the degree is equal to the number of adjacent vertices. :: (if loop is allowed, :: the number of edges and the number of adjacent vertices are different.) :: at first we defined degree(v), :: where v was Element of the SEdges of(G) and G was an implicit argument. :: but now we have changed the type of v to set, :: and G must be an explicit argument :: or we get an error "Inaccessible locus". definition let X be set, G be SimpleGraph of X; let v be set; func degree (G,v) -> Element of NAT means :Def8: ex X being finite set st ( for z being set holds (z in X iff z in (the SEdges of G) & v in z)) & it = card X; existence proof defpred X[set] means v in \$1; consider X being set such that A1: for z being set holds z in X iff z in the SEdges of G & X[z] from XFAMILY:sch 1; A2: X c= (the SEdges of G) by A1; (the SEdges of G) is finite by Th21; then reconsider X as finite set by A2; take card(X), X; thus thesis by A1; end; uniqueness proof let IT1, IT2 be Element of NAT; assume ( ex X1 be finite set st (for z being set holds (z in X1 iff z in the SEdges of G & v in z)) & IT1 = card(X1))& ex X2 be finite set st (for z being set holds (z in X2 iff z in the SEdges of G & v in z)) & IT2 = card(X2); then consider X1, X2 be finite set such that A3: for z being set holds (z in X1 iff z in the SEdges of G & v in z) and A4: IT1 = card(X1) and A5: for z being set holds (z in X2 iff z in the SEdges of G & v in z) and A6: IT2 = card(X2); A7: X2 c= X1 proof let z be object; reconsider zz=z as set by TARSKI:1; assume z in X2; then z in the SEdges of G & v in zz by A5; hence thesis by A3; end; X1 c= X2 proof let z be object; reconsider zz=z as set by TARSKI:1; assume z in X1; then z in the SEdges of G & v in zz by A3; hence thesis by A5; end; hence thesis by A4,A6,A7,XBOOLE_0:def 10; end; end; theorem Th28: for X being non empty set, G being SimpleGraph of X, v being set holds ex ww being finite set st ww = {w where w is Element of X : w in the carrier of G & {v,w} in the SEdges of G} & degree(G,v) = card ww proof let X be non empty set, G be SimpleGraph of X, v be set; set ww={w where w is Element of X: w in (the carrier of G) & {v,w} in (the SEdges of G)}; consider Y being finite set such that A1: for z being set holds (z in Y iff z in (the SEdges of G) & v in z) and A2: degree(G,v) = card(Y) by Def8; A3: for z being set holds (z in ww iff z in (the carrier of G) & {v,z} in ( the SEdges of G) ) proof let z be set; hereby assume z in ww; then ex w being Element of X st z=w & w in (the carrier of G) & {v,w} in ( the SEdges of G); hence z in (the carrier of G) & {v,z} in (the SEdges of G); end; thus z in (the carrier of G) & {v,z} in (the SEdges of G) implies z in ww proof assume A4: z in (the carrier of G) & {v,z} in (the SEdges of G); (the carrier of G) is finite Subset of X by Th21; hence thesis by A4; end; end; A5: ww c= (the carrier of G) by A3; (the carrier of G) is finite by Th21; then reconsider ww as finite set by A5; take ww; ww,Y are_equipotent proof set wwY = {[w,{v,w}] where w is Element of X : w in ww & {v,w} in Y}; take wwY; A6: for x,y,z,u being object st [x,y] in wwY & [z,u] in wwY holds (x = z iff y = u) proof let x,y,z,u be object; assume that A7: [x,y] in wwY and A8: [z,u] in wwY; consider w1 being Element of X such that A9: [x,y]=[w1,{v,w1}] and w1 in ww and A10: {v,w1} in Y by A7; consider w2 being Element of X such that A11: [z,u]=[w2,{v,w2}] and w2 in ww and {v,w2} in Y by A8; hereby assume A12: x=z; w1 = [w1,{v,w1}]`1 .= [x,y]`1 by A9 .= z by A12 .= [w2,{v,w2}]`1 by A11 .= w2; hence y = [w2,{v,w2}]`2 by A9 .= u by A11; end; hereby {v,w1} in (the SEdges of G) by A1,A10; then A13: v<>w1 by Th10; assume A14: y=u; {v,w1} = [w1,{v,w1}]`2 .= [x,y]`2 by A9 .= u by A14 .= [w2,{v,w2}]`2 by A11 .= {v,w2}; then w1=w2 by A13,ZFMISC_1:6; hence x = [z,u]`1 by A9,A11 .= z; end; end; A15: for w being set holds ([w,{v,w}] in wwY iff w in ww & {v,w} in Y) proof let w be set; hereby assume [w,{v,w}] in wwY; then consider w9 being Element of X such that A16: [w,{v,w}]=[w9,{v,w9}] and A17: w9 in ww & {v,w9} in Y; w = [w9,{v,w9}]`1 by A16 .= w9; hence w in ww & {v,w} in Y by A17; end; thus w in ww & {v,w} in Y implies [w,{v,w}] in wwY proof assume that A18: w in ww and A19: {v,w} in Y; A20: w in (the carrier of G) by A5,A18; (the carrier of G) is finite Subset of X by Th21; then reconsider w as Element of X by A20; ex z being Element of X st [w,{v,w}]=[z,{v,z}] & z in ww & {v,z} in Y by A18,A19; hence thesis; end; end; A21: for y being object st y in Y ex x being object st x in ww & [x,y] in wwY proof let y be object; assume A22: y in Y; then A23: y in (the SEdges of G) by A1; reconsider yy = y as set by TARSKI:1; A24: v in yy by A1,A22; ex w being set st w in (the carrier of G) & y={v,w} proof consider v1,v2 being object such that A25: v1 in (the carrier of G) and A26: v2 in (the carrier of G) and v1<>v2 and A27: y={v1,v2} by A23,Th8; per cases by A24,A27,TARSKI:def 2; suppose A28: v=v1; take v2; thus thesis by A26,A27,A28; end; suppose A29: v=v2; take v1; thus thesis by A27,A29,A25; end; end; then consider w being set such that A30: w in (the carrier of G) and A31: y={v,w}; take w; thus w in ww by A3,A23,A30,A31; hence thesis by A15,A22,A31; end; for x being object st x in ww ex y being object st y in Y & [x,y] in wwY proof let x be object; assume A32: x in ww; take {v,x}; A33: v in {v,x} by TARSKI:def 2; {v,x} in (the SEdges of G) by A3,A32; hence {v,x} in Y by A1,A33; hence thesis by A15,A32; end; hence thesis by A21,A6; end; hence thesis by A2,CARD_1:5; end; theorem for X being non empty set,g being SimpleGraph of X, v being set st v in the carrier of g holds ex VV being finite set st VV=(the carrier of g) & degree(g,v)<(card VV) proof let X be non empty set, g be SimpleGraph of X, v be set; reconsider VV=the carrier of g as finite set by Th21; consider ww being finite set such that A1: ww={w where w is Element of X : w in VV & {v,w} in the SEdges of g} and A2: degree(g,v)=card ww by Th28; assume A3: v in (the carrier of g); A4: now assume ww=VV; then A5: ex w being Element of X st v=w & w in VV & {v,w} in (the SEdges of g) by A3,A1; {v,v}={v} by ENUMSET1:29; then consider x,y being object such that x in VV and y in VV and A6: x<>y and A7: {v}={x,y} by A5,Th8; v=x by A7,ZFMISC_1:4; hence ww<>VV by A6,A7,ZFMISC_1:4; end; take VV; ww c= VV proof let e be object; assume e in ww; then ex w being Element of X st e=w & w in VV & {v,w} in (the SEdges of g) by A1; hence thesis; end; then ww c< VV by A4,XBOOLE_0:def 8; hence thesis by A2,CARD_2:48; end; theorem for g being SimpleGraph of X, v,e being set st e in the SEdges of g & degree (g,v)=0 holds not v in e proof let g be SimpleGraph of X, v,e be set; assume that A1: e in the SEdges of g and A2: degree(g,v)=0; consider Y be finite set such that A3: for z being set holds (z in Y iff z in the SEdges of g & v in z) and A4: degree(g,v)=card(Y) by Def8; assume v in e; then Y is non empty by A1,A3; hence contradiction by A2,A4; end; theorem for g being SimpleGraph of X, v being set, vg being finite set st vg=( the carrier of g) & v in vg & 1+degree(g,v)=(card vg) holds for w being Element of vg st v<>w holds ex e being set st e in (the SEdges of g) & e={v,w} proof let g be SimpleGraph of X, v be set, vg be finite set; assume that A1: vg=(the carrier of g) and A2: v in vg and A3: 1+degree(g,v)=(card vg); vg is Subset of X by A1,Th21; then reconsider X as non empty set by A2; let w be Element of vg; assume A4: v<>w; take {v,w}; hereby now consider ww being finite set such that A5: ww={vv where vv is Element of X : vv in vg & {v,vv} in (the SEdges of g) } and A6: degree(g,v)=(card ww) by A1,Th28; reconsider wwv=(ww \/ {v}) as finite set; assume A7: not {v,w} in (the SEdges of g); A8: not v in ww & not w in ww proof hereby assume v in ww; then ex vv being Element of X st v=vv & vv in vg & {v,vv} in (the SEdges of g) by A5; then {v} in (the SEdges of g) by ENUMSET1:29; then ex z being finite Subset of vg st {v}=z & (card z)=2 by A1,Th7; hence contradiction by CARD_1:30; end; assume w in ww; then ex vv being Element of X st w=vv & vv in vg & {v,vv} in (the SEdges of g) by A5; hence contradiction by A7; end; A9: now let e be object; assume e in ww; then ex vv being Element of X st e=vv & vv in vg & {v,vv} in (the SEdges of g) by A5; hence e in vg; end; wwv c= vg & wwv<>vg proof for e being object st e in {v} holds e in vg by A2,TARSKI:def 1; then A10: {v} c= vg; ww c= vg by A9; hence wwv c= vg by A10,XBOOLE_1:8; assume A11: wwv=vg; not w in {v} by A4,TARSKI:def 1; hence contradiction by A8,A11,XBOOLE_0:def 3; end; then A12: wwv c< vg by XBOOLE_0:def 8; (card wwv) = 1+(card ww) by A8,CARD_2:41; hence contradiction by A3,A6,A12,CARD_2:48; end; hence {v,w} in the SEdges of g; end; thus thesis; end; begin :: SECTION 7: path, cycle :: path is coded as a sequence of vertices, :: any two of them contained are different each other. :: but the head and the tail may be equal (which is cycle). definition let X be set, g be SimpleGraph of X, v1,v2 be Element of g, p be FinSequence of the carrier of g; pred p is_path_of v1,v2 means (p.1)=v1 & (p.(len p))=v2 & (for i being Element of NAT st (1<=i & i<(len p)) holds {p.i, p.(i+1)} in (the SEdges of g)) & for i,j being Element of NAT st 1<=i & i<(len p) & i p.j & {p.i,p.(i+1)}<>{p.j,p.(j+1)}; end; definition let X be set, g be SimpleGraph of X, v1,v2 be Element of (the carrier of g); func PATHS(v1,v2) -> Subset of ((the carrier of g)*) equals {ss where ss is Element of (the carrier of g)* : ss is_path_of v1,v2}; coherence proof set IT={ss where ss is Element of (the carrier of g)* : ss is_path_of v1, v2}; IT c= ((the carrier of g)*) proof let e be object; assume e in IT; then ex ss being Element of (the carrier of g)* st e=ss & ss is_path_of v1 ,v2; hence thesis; end; hence thesis; end; end; theorem for g being SimpleGraph of X, v1,v2 being Element of (the carrier of g ), e being set holds (e in PATHS(v1,v2) iff ex ss being Element of (the carrier of g)* st e=ss & ss is_path_of v1,v2 ); theorem for g being SimpleGraph of X, v1,v2 being Element of (the carrier of g ), e being Element of (the carrier of g)* st e is_path_of v1,v2 holds e in PATHS(v1,v2); ::definition :: is_cycle :: let g be SimpleGraph of X, :: v1,v2 be Element of (the carrier of g), :: p be Element of PATHS(v1,v2); :: pred p is_cycle means :cycleDef: :: v1=v2 & ex q being Element of ((the carrier of g)*) st (q=p & 3<=(len q)); ::end; definition let X be set, g be SimpleGraph of X, p be set; pred p is_cycle_of g means ex v being Element of (the carrier of g) st p in PATHS(v,v); end; :: cycle(v) = {v1,...,vn : {vi,v(i+1)} in EdgesOf g, 3 <= n} begin :: SECTION 8: some famous graphs. :: K_{3,3} = {{1,2,3,4,5,6}, :: {{1,4},{1,5},{1,6},{2,4},{2,5},{2,6},{3,4},{3,5},{3,6}}}. :: K_5 = {{1,2,3,4,5}, :: {{1,2},{1,3},{1,4},{1,5},{2,3},{2,4},{2,5},{3,4},{3,5},{4,5}}}. :: for the proof of Kuratowski's theorem, we need only K_{3,3} and K_5. :: here we define complete (and complete bipartate) graphs in general. definition let n,m be Element of NAT; func K_(m,n) -> SimpleGraph of NAT means ex ee being Subset of TWOELEMENTSETS(Seg (m+n)) st ee = {{i,j} where i,j is Element of NAT : i in ( Seg m) & j in (nat_interval(m+1,m+n))} & it = SimpleGraphStruct (# (Seg (m+n)), ee#); existence proof set VV = Seg (m+n), V1 = Seg m, V2 = nat_interval(m+1,m+n), EE = {{i,j} where i,j is Element of NAT : i in V1 & j in V2}; m<=(m+n) by NAT_1:11; then A1: V1 c= VV by FINSEQ_1:5; A2: V2 c= VV by Th4,NAT_1:11; EE c= TWOELEMENTSETS(VV) proof let e be object; reconsider ee=e as set by TARSKI:1; assume e in EE; then consider i0,j0 being Element of NAT such that A3: e = {i0,j0} and A4: i0 in V1 & j0 in V2; i0 in VV & j0 in VV by A1,A2,A4; then for e0 being object st e0 in ee holds e0 in VV by A3,TARSKI:def 2; then A5: ee c= VV; mj0 by A4,XBOOLE_0:def 4; hence thesis by A1,A2,A3,A4,A5,Th8; end; then reconsider EE as finite Subset of TWOELEMENTSETS(VV) by Th13, FINSET_1:1; set IT = SimpleGraphStruct (# VV, EE #); IT in SIMPLEGRAPHS(NAT); then reconsider IT as SimpleGraph of NAT by Def4; reconsider EE as Subset of TWOELEMENTSETS(Seg (m+n)); take IT,EE; thus thesis; end; uniqueness; end; definition let n be Element of NAT; func K_(n) -> SimpleGraph of NAT means :Def13: ex ee being finite Subset of TWOELEMENTSETS(Seg n) st ee = {{i,j} where i,j is Element of NAT : i in (Seg n) & j in (Seg n) & i<>j} & it = SimpleGraphStruct (# (Seg n), ee #); existence proof set EE = {{i,j} where i,j is Element of NAT : i in Seg n & j in Seg n & i <>j}; now let e be object; reconsider ee=e as set by TARSKI:1; assume e in EE; then consider i0,j0 being Element of NAT such that A1: e={i0,j0} and A2: i0 in Seg n and A3: j0 in Seg n and A4: i0<>j0; ee c= (Seg n) proof let e0 be object; assume A5: e0 in ee; per cases by A1,A5,TARSKI:def 2; suppose e0 = i0; hence thesis by A2; end; suppose e0 = j0; hence thesis by A3; end; end; hence e in TWOELEMENTSETS(Seg n) by A1,A2,A3,A4,Th8; end; then EE c= TWOELEMENTSETS(Seg n); then reconsider EE as finite Subset of TWOELEMENTSETS(Seg n) by Th13, FINSET_1:1; set IT = SimpleGraphStruct (# Seg n,EE #); IT in SIMPLEGRAPHS(NAT); then reconsider IT as SimpleGraph of NAT by Def4; take IT,EE; thus thesis; end; uniqueness; end; :: TriangleGraph will be used in the definition of planegraphs. definition func TriangleGraph -> SimpleGraph of NAT equals K_(3); correctness; end; theorem Th34: ex ee being Subset of TWOELEMENTSETS(Seg 3) st ee = {.{.1,2.},{. 2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct (#(Seg 3),ee#) proof consider ee being finite Subset of TWOELEMENTSETS(Seg 3) such that A1: ee = {{i,j} where i,j is Element of NAT : i in (Seg 3) & j in (Seg 3 ) & i<>j} and A2: TriangleGraph = SimpleGraphStruct (#(Seg 3),ee#) by Def13; take ee; now let a be object; assume a in ee; then consider i,j being Element of NAT such that A3: a={i,j} and A4: i in (Seg 3) and A5: j in (Seg 3) and A6: i<>j by A1; per cases by A4,ENUMSET1:def 1,FINSEQ_3:1; suppose A7: i=1; now per cases by A5,ENUMSET1:def 1,FINSEQ_3:1; suppose j=1; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6,A7; end; suppose j=2; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3,A7,ENUMSET1:def 1; end; suppose j=3; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3,A7,ENUMSET1:def 1; end; end; hence a in {.{.1,2.},{.2,3.},{.3,1.}.}; end; suppose A8: i=2; now per cases by A5,ENUMSET1:def 1,FINSEQ_3:1; suppose j=1; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3,A8,ENUMSET1:def 1; end; suppose j=2; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6,A8; end; suppose j=3; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3,A8,ENUMSET1:def 1; end; end; hence a in {.{.1,2.},{.2,3.},{.3,1.}.}; end; suppose A9: i=3; now per cases by A5,ENUMSET1:def 1,FINSEQ_3:1; suppose j=1; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3,A9,ENUMSET1:def 1; end; suppose j=2; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3,A9,ENUMSET1:def 1; end; suppose j=3; hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6,A9; end; end; hence a in {.{.1,2.},{.2,3.},{.3,1.}.}; end; end; then A10: ee c= {.{.1,2.},{.2,3.},{.3,1.}.}; now let e be object; assume A11: e in {.{.1,2.},{.2,3.},{.3,1.}.}; per cases by A11,ENUMSET1:def 1; suppose A12: e={1,2}; now take i=1,j=2; thus e={i,j} by A12; thus i in Seg 3 & j in (Seg 3); thus i<>j; end; hence e in ee by A1; end; suppose A13: e={2,3}; now take i=2,j=3; thus e={i,j} & i in (Seg 3) & j in (Seg 3) & i<>j by A13; end; hence e in ee by A1; end; suppose A14: e={3,1}; now take i=3,j=1; thus e={i,j} & i in (Seg 3) & j in (Seg 3) & i<>j by A14; end; hence e in ee by A1; end; end; then {.{.1,2.},{.2,3.},{.3,1.}.} c= ee; hence thesis by A2,A10,XBOOLE_0:def 10; end; theorem (the carrier of TriangleGraph)=(Seg 3) & (the SEdges of TriangleGraph) = {.{.1,2.},{.2,3.},{.3,1.}.} by Th34; theorem {1,2} in (the SEdges of TriangleGraph) & {2,3} in (the SEdges of TriangleGraph) & {3,1} in (the SEdges of TriangleGraph) by Th34,ENUMSET1:def 1; theorem <*1*>^<*2*>^<*3*>^<*1*> is_cycle_of TriangleGraph proof reconsider o=1 as Element of (the carrier of TriangleGraph) by Th34, ENUMSET1:def 1,FINSEQ_3:1; reconsider VERTICES = (the carrier of TriangleGraph) as non empty set by Th34 ; set p = <*1*>^<*2*>^<*3*>^<*1*>; A1: p.1 = 1 by FINSEQ_1:66; reconsider One=1, Two=2, Three=3 as Element of VERTICES by Th34, ENUMSET1:def 1,FINSEQ_3:1; A2: p.2 = 2 by FINSEQ_1:66; reconsider ONE=<*One*>, TWO=<*Two*>, THREE=<*Three*> as FinSequence of (the carrier of TriangleGraph); p = ONE^TWO^THREE^ONE; then reconsider pp=p as Element of (the carrier of TriangleGraph)* by FINSEQ_1:def 11; A3: p.3 = 3 by FINSEQ_1:66; A4: p.4 = 1 by FINSEQ_1:66; A5: now let i be Element of NAT; assume that A6: 1<=i and A7: i<(len p); i<3+1 by A7,FINSEQ_1:66; then i<=3 by NAT_1:13; then A8: i in Seg 3 by A6; per cases by A8,ENUMSET1:def 1,FINSEQ_3:1; suppose i=1; hence {pp.i, pp.(i+1)} in (the SEdges of TriangleGraph) by A1,A2,Th34, ENUMSET1:def 1; end; suppose i=2; hence {pp.i, pp.(i+1)} in (the SEdges of TriangleGraph ) by A2,A3,Th34, ENUMSET1:def 1; end; suppose i=3; hence {pp.i, pp.(i+1)} in (the SEdges of TriangleGraph ) by A3,A4,Th34, ENUMSET1:def 1; end; end; A9: now let i,j be Element of NAT; assume that A10: 1<=i and A11: ipp.j by A19,FINSEQ_1:66; thus {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)} by A1,A2,A3,A18,A21,ZFMISC_1:6; end; suppose A22: j=3; hence pp.i<>pp.j by A19,FINSEQ_1:66; thus {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)} by A1,A2,A3,A18,A22,ZFMISC_1:6; end; end; hence pp.i <> pp.j & {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)}; end; suppose A23: i=2; then j=3 by A14,A17,XXREAL_0:1; hence pp.i <> pp.j & {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)} by A2,A3,A4,A23, ZFMISC_1:6; end; suppose i=3; hence pp.i <> pp.j & {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)} by A12,A16,NAT_1:13 ; end; end; (len p) = 4 by FINSEQ_1:66; then pp is_path_of o,o by A1,A4,A5,A9; then pp in PATHS(o,o); hence thesis; end;