Copyright (c) 1994 Association of Mizar Users
environ
vocabulary FINSEQ_1, BOOLE, FINSET_1, FUNCT_1, CARD_1, REALSET1, SETWISEO,
FINSUB_1, TARSKI, MCART_1, SGRAPH1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
MCART_1, CARD_1, STRUCT_0, REALSET1, FUNCT_1, FUNCT_2, FINSEQ_1,
FINSET_1, FINSEQ_2, FINSUB_1, SETWISEO;
constructors MCART_1, WELLORD2, REALSET1, NAT_1, SETWISEO, FINSEQ_2, XREAL_0,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, FINSET_1, FINSUB_1, REALSET1, RELSET_1, FINSEQ_1, ARYTM_3,
MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
theorems AXIOMS, TARSKI, ENUMSET1, ZFMISC_1, REAL_1, NAT_1, FINSEQ_1,
FINSEQ_3, FINSUB_1, REALSET1, MCART_1, CARD_1, CARD_2, FINSET_1, SCM_1,
GROUP_3, XBOOLE_0, XBOOLE_1;
schemes SETWISEO, XBOOLE_0;
begin
Lm1: for e being set, n being Nat st e in Seg n holds
ex i being Nat st (e=i & 1<=i & i<=n)
proof let e be set, n be Nat; assume A1: e in Seg n;
then reconsider e as Nat;
take e; thus thesis by A1,FINSEQ_1:3;
end;
:: 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 :Def1:
{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 set; assume e in IT;
then consider i being Nat such that A1: i=e & m<=i & 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 2;
suppose i<>0; then 0<i by NAT_1:19; then (0+1)<=i by NAT_1:38;
then e in (Seg n) by A1,FINSEQ_1:3;
hence e in ({0} \/ (Seg n)) by XBOOLE_0:def 2;
end;
hence e in ({0} \/ (Seg n));
end;
then A2: IT c= ({0} \/ (Seg n)) by TARSKI:def 3; {0} c= NAT by ZFMISC_1:37
;
then {0}\/(Seg n) c= NAT by XBOOLE_1:8;
hence IT is Subset of NAT by A2,XBOOLE_1:1;
end;
end;
definition let m,n be Nat;
cluster nat_interval(m,n) -> finite;
coherence proof
set IT = {i where i is Nat : m<=i & i<=n};
A1: IT = nat_interval(m,n) by Def1;
now let e be set; assume e in IT;
then consider i being Nat such that A2: i=e & m<=i & i<=n;
now per cases;
suppose i=0; then i in {0} by TARSKI:def 1;
hence e in ({0}\/(Seg n)) by A2,XBOOLE_0:def 2;
suppose i<>0; then 0<i by NAT_1:19; then (0+1)<=i by NAT_1:38;
then e in (Seg n) by A2,FINSEQ_1:3;
hence e in ({0} \/ (Seg n)) by XBOOLE_0:def 2;
end;
hence e in ({0} \/ (Seg n));
end;
then IT c= ({0} \/ (Seg n)) by TARSKI:def 3;
hence thesis by A1,FINSET_1:13;
end;
end;
canceled;
theorem Th2:
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)
proof let m,n be Nat, e be set;
hereby assume e in nat_interval(m,n);
then e in {i where i is Nat : m<=i & i<=n} by Def1;
hence ex i being Nat st (e=i & m<=i & i<=n);
end;
assume ex i being Nat st (e=i & m<=i & i<=n);
then e in {i where i is Nat : m<=i & i<=n};
hence thesis by Def1;
end;
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 consider i being Nat such that A1: k=i & m<=i & i<=n by Th2;
thus m<=k & k<=n by A1;
end;
assume m <= k & k <= n; hence thesis by Th2;
end;
theorem
for n being Nat holds nat_interval (1,n) = Seg n
proof let n be Nat;
A1: now let e be set; assume e in nat_interval (1,n);
then consider i being Nat such that A2: (e=i & 1<=i & i<=n) by Th2;
thus e in Seg n by A2,FINSEQ_1:3;
end;
now let e be set; assume A3: e in Seg n;
then reconsider i = e as Nat; 1 <= i & i <= n by A3,FINSEQ_1:3;
hence e in nat_interval(1,n) by Th2;
end;
then nat_interval (1,n) c= Seg n & Seg n c= nat_interval (1,n)
by A1,TARSKI:def 3;
hence thesis by XBOOLE_0:def 10;
end;
theorem Th5:
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 set; assume e in nat_interval(m,n);
then consider i being Nat such that A2: (e=i & m<=i & i<=n) by Th2;
1<=i by A1,A2,AXIOMS:22; hence e in Seg n by A2,FINSEQ_1:3;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th6: for k,m,n being Nat st k<m holds
Seg k misses nat_interval(m,n)
proof let k,m,n be Nat; assume A1: k<m;
now let e be set; assume e in ((Seg k) /\ nat_interval(m,n));
then A2: e in (Seg k) & e in nat_interval(m,n) by XBOOLE_0:def 3;
then consider i being Nat such that A3: (e=i & 1<=i & i<=k) by Lm1;
consider j being Nat such that A4: (e=j & m<=j & j<=n) by A2,Th2;
thus e in {} by A1,A3,A4,AXIOMS:22;
end;
then ((Seg k) /\ nat_interval(m,n)) c= {} by TARSKI:def 3;
then ((Seg k) /\ nat_interval(m,n)) = {} by XBOOLE_1:3;
hence thesis by XBOOLE_0:def 7;
end;
theorem for m,n being Nat st n<m holds nat_interval(m,n)={}
proof let m,n be Nat; assume A1: n<m;
now let e be set; assume e in nat_interval(m,n);
then consider i being Nat such that A2: e=i & m<=i & i<=n
by Th2;
thus contradiction by A1,A2,AXIOMS:22;
end;
hence thesis by XBOOLE_0:def 1;
end;
Lm2:
for A being set, s being Element of bool A, n being set st n in A holds
s \/ {n} is Element of bool A
proof
let A be set, s be Element of bool A, n be set; assume A1: n in A;
s \/ {n} c= A proof
let m be set; assume A2: m in (s \/ {n});
now per cases by A2,XBOOLE_0:def 2;
suppose m in s; hence m in A;
suppose m in {n}; hence m in A by A1,TARSKI:def 1;
end;
hence m in A;
end;
hence thesis;
end;
definition let A be set;
canceled 2;
func TWOELEMENTSETS(A) -> set equals :Def4:
{z where z is finite Element of bool A : card z = 2};
coherence;
end;
canceled;
theorem Th9: 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))
proof let A be set;
TWOELEMENTSETS(A) =
{z where z is finite Element of bool A : (card z)=2}
by Def4;
hence thesis;
end;
theorem Th10: for A be set, e be set holds
(e in TWOELEMENTSETS(A) iff
(e is finite Subset of A &
ex x,y being set 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 consider z being finite Subset of A such that A1:
(e=z & (card z)=2) by Th9;
thus e is finite Subset of A by A1;
reconsider e'=e as finite Subset of A by A1;
consider x,y being set such that A2:
x<>y & e'={x,y} by A1,GROUP_3:166;
take x,y;
x in e' & y in e' by A2,TARSKI:def 2;
hence x in A & y in A;
thus x<>y & e={x,y} by A2;
end;
assume e is finite Element of bool A &
ex x,y being set st (x in A & y in A & x<>y & e={x,y});
then consider x,y being Element of A such that
A3: (x in A & y in A & not x=y & e={x,y});
reconsider xy = {x,y} as finite Element of bool A by A3,ZFMISC_1:38;
ex z being finite Element of bool A st (e=z & (card z)=2)
proof
take xy; thus e=xy by A3; thus (card xy)=2 by A3,CARD_2:76;
end;
hence thesis by Th9;
end;
theorem Th11: for A being set holds TWOELEMENTSETS(A) c= (bool A)
proof let A be set;
now let x be set; assume x in TWOELEMENTSETS(A);
then x is finite Element of (bool A) &
ex u,v being set st (u in A & v in A & u<>v & x={u,v}) by Th10;
hence x in (bool A);
end;
hence thesis by TARSKI:def 3;
end;
theorem Th12: 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 set such that A2:
(x in A & y in A & not x=y & {e1,e2} = {x,y}) by Th10;
per cases by A2,ZFMISC_1:10;
suppose (e1=x & e2=x); then {x} in TWOELEMENTSETS(A) by A1,ENUMSET1:69;
then consider x1,x2 being set such that A3:
(x1 in A & x2 in A & not x1=x2 & {x} = {x1,x2}) by Th10;
thus e1 in A & e2 in A & (not e1=e2) by A3,ZFMISC_1:9;
suppose (e1=x & e2=y); hence e1 in A & e2 in A & not e1=e2 by A2;
suppose (e1=y & e2=x); hence e1 in A & e2 in A & not e1=e2 by A2;
suppose (e1=y & e2=y);
then {y} in TWOELEMENTSETS(A) by A1,ENUMSET1:69;
then consider x1,x2 being set such that A4:
(x1 in A & x2 in A & (not x1=x2) & {y}={x1,x2}) by Th10;
thus e1 in A & e2 in A & not e1=e2 by A4,ZFMISC_1:9;
end;
theorem Th13: TWOELEMENTSETS {} = {}
proof
A1: TWOELEMENTSETS {} c= {} proof
let a be set; assume a in TWOELEMENTSETS({});
then consider a1,a2 being set such that A2:
(a1 in {} & a2 in {} & not a1=a2 & a = {a1,a2}) by Th10;
thus a in {} by A2; end;
{} c= TWOELEMENTSETS({}) by XBOOLE_1:2;
hence thesis by A1,XBOOLE_0:def 10;
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 set; assume A2: e in TWOELEMENTSETS(t);
then A3: e is finite Element of bool t &
ex x,y being set st (x in t & y in t & (not x=y) & e={x,y})
by Th10;
consider x,y being set such that
A4: (x in t & y in t & (not x=y) & e={x,y}) by A2,Th10;
e is finite Element of bool u by A1,A3,XBOOLE_1:1;
hence thesis by A1,A4,Th10;
end;
theorem Th15:
for A being finite set holds TWOELEMENTSETS(A) is finite
proof let A be finite set; A1: (bool A) is finite by FINSET_1:24;
TWOELEMENTSETS(A) c= bool A by Th11;
hence thesis by A1,FINSET_1:13;
end;
theorem for A being non trivial set holds
TWOELEMENTSETS(A) is non empty
proof let A be non trivial set;
consider a being set such that A1: a in A by XBOOLE_0:def 1;
reconsider A' = A as non empty non trivial set;
(A'\{a}) is non empty set by REALSET1:32;
then consider b being set such that A2: b in (A'\{a}) by XBOOLE_0:def 1;
A3: b in A' & not b in {a} by A2,XBOOLE_0:def 4;
then A4: a in A & b in A & a<>b by A1,TARSKI:def 1;
{a,b} c= A by A1,A3,ZFMISC_1:38;
hence thesis by A4,Th10;
end;
theorem
for a being set holds TWOELEMENTSETS {a} = {}
proof let a be set;
now let x be set; assume x in TWOELEMENTSETS({a});
then consider u,v being set such that A1:
(u in {a} & v in {a} & u<>v & x = {u,v}) by Th10;
u = a by A1,TARSKI:def 1
.= v by A1,TARSKI:def 1;
hence contradiction by A1;
end;
hence thesis by XBOOLE_0:def 1;
end;
definition let X be empty set;
cluster -> empty Subset of X;
coherence by XBOOLE_1:3;
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 <Empty,Empty>,
:: (2) if <V,E> is an element of SIMPLEGRAPHS and n is not a vertex of <V,E>,
:: then <(V U {n}),E> is also an element of SIMPLEGRAPHS,
:: (3) if <V,E> is an element of SIMPLEGRAPHS,
:: v1,v2 are different vertices of <V,E>,
:: and {v1,v2} is not an edge of <V,E>,
:: then <V,(E U {v1,v2})> is also an element of SIMPLEGRAPHS.
definition let X be set;
canceled;
func SIMPLEGRAPHS(X) -> set equals :Def6:
{SimpleGraphStruct (# v,e #)
where v is finite Subset of X,
e is finite Subset of TWOELEMENTSETS(v) :
not contradiction};
coherence;
end;
canceled;
theorem Th19:
SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) in SIMPLEGRAPHS(X)
proof
reconsider phiv = {} as finite Element of bool X by XBOOLE_1:2;
reconsider phie = {}TWOELEMENTSETS{}
as finite Subset of TWOELEMENTSETS(phiv);
SimpleGraphStruct (#phiv,phie#) in {SimpleGraphStruct (# v,e #)
where v is finite Subset of X,
e is finite Subset of TWOELEMENTSETS(v) :
not contradiction};
hence SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) in SIMPLEGRAPHS(X)
by Def6;
end;
definition let X be set;
cluster SIMPLEGRAPHS(X) -> non empty;
coherence by Th19;
end;
definition let X be set;
mode SimpleGraph of X -> strict SimpleGraphStruct means :Def7:
it is Element of SIMPLEGRAPHS(X);
existence proof
take SimpleGraphStruct (# {},{}TWOELEMENTSETS{} #); thus thesis by Th19;
end;
end;
canceled;
theorem Th21: for g being set 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#))
proof let g be set;
hereby assume g in SIMPLEGRAPHS(X);
then g in {SimpleGraphStruct (# v,e #) where
v is finite Subset of X,
e is finite Subset of TWOELEMENTSETS(v) : not contradiction}
by Def6;
hence ex v being finite Element of bool X,
e being finite Subset of TWOELEMENTSETS(v) st
g = SimpleGraphStruct (#v,e#);
end;
given v being finite Element of bool X,
e being finite Subset of TWOELEMENTSETS(v) such that
A1: g = SimpleGraphStruct (#v,e#);
g in {SimpleGraphStruct (# v',e' #) where
v' is finite Subset of X,
e' is finite Subset of TWOELEMENTSETS(v') : not contradiction}
by A1;
hence g in SIMPLEGRAPHS(X) by Def6;
end;
begin :: SECTION 2: destructors for SimpleGraphStruct.
canceled;
theorem Th23:
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 Def7;
then consider v being finite Element of bool X,
e being finite Subset of TWOELEMENTSETS(v) such that
A1: g = SimpleGraphStruct (#v,e#) by Th21;
thus (the carrier of g) c= X by A1;
thus thesis;
end;
canceled;
theorem
for g being SimpleGraph of X, e being set st e in the SEdges of g holds
ex v1,v2 being set st
(v1 in the carrier of g & v2 in the carrier of g &
v1 <> v2 & e={v1,v2}) by Th10;
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 Th12;
theorem Th27: 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 Def7;
then consider v being finite Subset of X,
e being finite Subset of TWOELEMENTSETS(v) such that A1:
g = SimpleGraphStruct (#v,e#) by Th21;
thus thesis by A1;
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,G' be SimpleGraph of X;
pred G is_isomorphic_to G' means
ex Fv being Function of the carrier of G, the carrier of G' 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 consider
v being finite Element of bool X(),
e being finite Subset of TWOELEMENTSETS(v) such that
A5: g = SimpleGraphStruct (#v,e#) by Th21;
reconsider G = g as SimpleGraph of X() by A4,A5,Def7;
A6: (the carrier of G) c= X() &
(the SEdges of G) c= TWOELEMENTSETS(the carrier of G) by Th23;
per cases;
suppose A7: X() is empty;
then (the SEdges of G) is Subset of {} by A6,Th13,XBOOLE_1:3;
hence P[g] by A1,A6,A7,XBOOLE_1:3;
suppose X() is not empty;
:: now we treat only finite graphs and X() is non empty, so
:: we can use FinSubInd1 on (the carrier of G).
then reconsider X = X() as non empty set;
defpred X[set] means P[SimpleGraphStruct (#$1,{}TWOELEMENTSETS($1)#)];
A8: X[{}.X] by A1;
A9: now
let B' be (Element of Fin X), b be Element of X;
assume A10: X[B'] & not b in B';
set g= SimpleGraphStruct (#B',{}TWOELEMENTSETS(B')#);
B' is finite Subset of X by FINSUB_1:32;
then A11: g in SIMPLEGRAPHS(X()) by Th21;
then reconsider g as SimpleGraph of X() by Def7;
P[SimpleGraphStruct (#(the carrier of g)\/{b},
{}TWOELEMENTSETS((the carrier of g)\/{b})#)] by A2,A10,A11;
hence X[B' \/ {b}];
end;
A12: for VV being Element of Fin X holds X[VV] from FinSubInd1(A8,A9);
A13: now let VV be Element of (Fin X);
per cases;
suppose A14: TWOELEMENTSETS(VV) = {};
let EEa be Finite_Subset of TWOELEMENTSETS(VV),
EE be Subset of TWOELEMENTSETS(VV);
assume EEa = EE; EE = {}TWOELEMENTSETS(VV) by A14,XBOOLE_1:3;
hence P[SimpleGraphStruct (#VV,EE#)] by A12;
suppose TWOELEMENTSETS(VV) <> {};
then reconsider TT = TWOELEMENTSETS(VV) as non empty set;
defpred Q[Finite_Subset of TT] means
for EE being Subset of TWOELEMENTSETS(VV) st EE = $1 holds
P[SimpleGraphStruct (#VV,EE#)];
A15: Q[{}.TT] proof let EE be Subset of TWOELEMENTSETS(VV);
assume EE = {}.TT; then EE = {}TWOELEMENTSETS(VV);
hence P[SimpleGraphStruct (#VV,EE#)] by A12;
end;
A16: now let ee be Finite_Subset of TT,
vv be Element of TT such that A17: Q[ee] & not vv in ee;
reconsider ee' = ee as Subset of TWOELEMENTSETS(VV)
by FINSUB_1:32;
A18: VV is finite Subset of X() by FINSUB_1:32;
set g = SimpleGraphStruct (#VV,ee'#);
g is Element of SIMPLEGRAPHS(X()) by A18,Th21;
then reconsider g as SimpleGraph of X() by Def7;
P[g] by A17;
then consider sege being Subset of TWOELEMENTSETS(the carrier of g)
such that A19: sege=((the SEdges of g)\/{vv}) and
A20: P[SimpleGraphStruct (#(the carrier of g),sege#)]
by A3,A17;
thus Q[ee \/ {vv}] by A19,A20;
end;
for EE being Finite_Subset of TT holds
Q[EE] from FinSubInd1(A15,A16);
hence for EE being Finite_Subset of TWOELEMENTSETS(VV),
EE' being Subset of TWOELEMENTSETS(VV) st EE' = EE holds
P[SimpleGraphStruct (#VV,EE'#)];
end;
A21: (the carrier of G) is Finite_Subset of X by A5,FINSUB_1:def 5;
(the SEdges of G) is
Finite_Subset of TWOELEMENTSETS(the carrier of G) by A5,FINSUB_1:def 5;
hence P[g] by A13,A21;
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,Th13,XBOOLE_1:3;
thus g=SimpleGraphStruct (#(the carrier of g),(the SEdges of g)#);
end;
canceled;
theorem Th30:
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 & not n in V) 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 A1: g in SIMPLEGRAPHS(X) & n in X & not n in V;
then reconsider g as SimpleGraph of X by Def7;
V = (the carrier of g);
then V is finite Subset of X by Th27;
then (V \/ {n}) is finite Element of (bool X)
by A1,Lm2,FINSET_1:14;
hence SimpleGraphStruct (#(V \/ {n}),Evn#) in SIMPLEGRAPHS(X)
by Th21;
end;
theorem Th31:
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 A1: (v1 in V & v2 in V) & (not v1=v2) & g in SIMPLEGRAPHS(X);
then reconsider g as SimpleGraph of X by Def7;
A2: (the carrier of g) is finite Subset of X &
(the SEdges of g) is finite Subset of TWOELEMENTSETS(V)
by Th27;
then reconsider V as finite Subset of X;
(E \/ {{v1,v2}}) c= TWOELEMENTSETS(V) & (E \/ {{v1,v2}}) is finite
proof
hereby let e be set; assume A3: e in E \/ {{v1,v2}}; per cases by A3,
XBOOLE_0:def 2;
suppose e in E;
hence e in TWOELEMENTSETS(V);
suppose e in {{v1,v2}};
then A4: v1 in V & v2 in V & v1<>v2 & e={v1,v2} by A1,TARSKI:def 1;
then e is Subset of V by ZFMISC_1:38;
hence e in TWOELEMENTSETS(V) by A4,Th10;
end;
thus (E \/ {{v1,v2}}) is finite by A2,FINSET_1:14;
end;
then reconsider E' = (E \/ {{v1,v2}})
as finite Subset of TWOELEMENTSETS(V);
SimpleGraphStruct (#V,E'#) in SIMPLEGRAPHS(X) by Th21;
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 :Def9:
(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;
canceled 3;
theorem Th35:
SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X
proof
thus SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) in SIMPLEGRAPHS(X)
by Th19;
thus
(for VV being Subset of X, EE being Subset of TWOELEMENTSETS(VV),
nn being set,
EEvn being finite Subset of TWOELEMENTSETS(VV \/ {nn}) st
(SimpleGraphStruct (#VV,EE#) in SIMPLEGRAPHS(X) &
nn in X & not nn in VV) holds
SimpleGraphStruct (#(VV \/ {nn}),EEvn#) in SIMPLEGRAPHS(X))
by Th30;
thus for V being Subset of X, E being Subset of TWOELEMENTSETS(V),
v1,v2 being set st
(SimpleGraphStruct (#V,E#) in SIMPLEGRAPHS(X) &
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 SIMPLEGRAPHS(X)
by Th31;
end;
theorem Th36:
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;
then A2: X[SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#)] by Def9;
A3: 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 A4:
g in SIMPLEGRAPHS(X) & g in OTHER & v in X &
not v in (the carrier of g);
set SVg=(the carrier of g), SEg=(the SEdges of g);
SVg is Subset of X & SEg is Subset of TWOELEMENTSETS(SVg)
by Th27;
hence SimpleGraphStruct (#(SVg \/ {v}),
{}TWOELEMENTSETS(SVg \/ {v})#) in OTHER
by A1,A4,Def9;
end;
A5: 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 A6: g in OTHER & e in TWOELEMENTSETS(the carrier of g) &
not e in (the SEdges of g);
set SVg = (the carrier of g), SEg = (the SEdges of g);
A7: SVg is finite Subset of X &
SEg is finite Subset of TWOELEMENTSETS(SVg) by Th27;
consider v1,v2 being set such that
A8: v1 in SVg & v2 in SVg & v1<>v2 & e={v1,v2} by A6,Th10;
consider v1v2 being finite Subset of TWOELEMENTSETS(SVg) such that
A9: v1v2=(SEg \/ {{v1,v2}}) & SimpleGraphStruct (#SVg,v1v2#) in OTHER
by A1,A6,A7,A8,Def9;
take v1v2;
thus v1v2=(SEg \/ {e}) & SimpleGraphStruct (#SVg,v1v2#) in OTHER
by A8,A9;
end;
A10: for e being set st e in SIMPLEGRAPHS(X) holds X[e]
from IndSimpleGraphs0(A2,A3,A5);
let e be set; assume e in SIMPLEGRAPHS(X); hence e in OTHER by A10;
end;
theorem
SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X &
for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS(X) c= OTHER by Th35,Th36;
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) -> Nat means :Def11:
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 Separation;
A2: (the SEdges of G) is finite by Th27;
X c= (the SEdges of G) proof
let z be set; assume z in X; hence z in (the SEdges of G) by A1; end;
then reconsider X as finite set by A2,FINSET_1:13;
take card(X), X; thus thesis by A1;
end;
uniqueness proof
let IT1, IT2 be 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)) & IT1 = card(X1) &
(for z being set holds
(z in X2 iff z in the SEdges of G & v in z)) & IT2 = card(X2);
A4: X1 c= X2 proof let z be set; assume z in X1;
then z in the SEdges of G & v in z by A3; hence z in X2 by A3;
end;
X2 c= X1 proof let z be set; assume z in X2;
then z in the SEdges of G & v in z by A3; hence z in X1 by A3;
end;
hence thesis by A3,A4,XBOOLE_0:def 10;
end;
end;
canceled;
theorem Th39:
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;
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)) &
degree(G,v) = card(Y) by Def11;
set ww={w where w is Element of X:
w in (the carrier of G) & {v,w} in (the SEdges of G)};
A2: 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 consider w being Element of X such that A3:
(z=w & w in (the carrier of G) & {v,w} in (the SEdges of G));
thus z in (the carrier of G) & {v,z} in (the SEdges of G) by A3;
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 Th27;
hence z in ww by A4;
end;
end;
A5: (the carrier of G) is finite by Th27;
A6: ww c= (the carrier of G)
proof let z be set; assume z in ww;
hence z in (the carrier of G) by A2; end;
then reconsider ww as finite set by A5,FINSET_1:13;
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};
A7: 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 w' being Element of X such that A8:
[w,{v,w}]=[w',{v,w'}] & w' in ww & {v,w'} in Y;
w = [w',{v,w'}]`1 by A8,MCART_1:7
.= w' by MCART_1:7;
hence (w in ww & {v,w} in Y) by A8; end;
thus (w in ww & {v,w} in Y) implies [w,{v,w}] in wwY proof
assume A9: (w in ww & {v,w} in Y);
(the carrier of G) is finite Subset of X by Th27;
then w in (the carrier of G) & (the carrier of G) c= X
by A6,A9;
then reconsider w as Element of X;
ex z being Element of X st
([w,{v,w}]=[z,{v,z}] & z in ww & {v,z} in Y) by A9;
hence thesis;
end;
end;
A10: (for x being set st x in ww ex y being set st y in Y & [x,y] in wwY)
proof let x be set; assume A11: x in ww;
then A12: x in (the carrier of G) & {v,x} in (the SEdges of G) by A2
;
A13: v in {v,x} by TARSKI:def 2;
take {v,x}; thus {v,x} in Y by A1,A12,A13;
hence [x,{v,x}] in wwY by A7,A11;
end;
A14: (for y being set st y in Y ex x being set st x in ww & [x,y] in wwY)
proof let y be set; assume A15: y in Y;
then A16: y in (the SEdges of G) & v in y by A1;
ex w being set st w in (the carrier of G) & y={v,w} proof
consider v1,v2 being set such that A17:
(v1 in (the carrier of G) & v2 in (the carrier of G) &
v1<>v2 & y={v1,v2}) by A16,Th10;
per cases by A16,A17,TARSKI:def 2;
suppose A18: v=v1; take v2;
thus v2 in (the carrier of G) & y={v,v2} by A17,A18;
suppose A19: v=v2; take v1;
thus v1 in (the carrier of G) by A17;
thus y= {v,v1} by A17,A19;
end;
then consider w being set such that A20:
w in (the carrier of G) & y={v,w};
take w;
thus w in ww by A2,A16,A20;
hence [w,y] in wwY by A7,A15,A20;
end;
A21: for x,y,z,u being set st [x,y] in wwY & [z,u] in wwY holds
(x = z iff y = u) proof
let x,y,z,u be set; assume A22: [x,y] in wwY & [z,u] in wwY;
then consider w1 being Element of X such that A23:
([x,y]=[w1,{v,w1}] & w1 in ww & {v,w1} in Y);
consider w2 being Element of X such that A24:
([z,u]=[w2,{v,w2}] & w2 in ww & {v,w2} in Y) by A22;
hereby assume A25: x=z;
w1 = [x,y]`1 by A23,MCART_1:7
.= z by A25,MCART_1:7
.= [w2,{v,w2}]`1 by A24,MCART_1:7
.= w2 by MCART_1:7;
hence y = [w2,{v,w2}]`2 by A23,MCART_1:7
.= u by A24,MCART_1:7;
end;
hereby assume A26: y=u;
A27:
{v,w1} = [x,y]`2 by A23,MCART_1:7
.= u by A26,MCART_1:7
.= [w2,{v,w2}]`2 by A24,MCART_1:7
.= {v,w2} by MCART_1:7;
{v,w1} in (the SEdges of G) by A1,A23;
then v<>w1 by Th12;
then w1=w2 by A27,ZFMISC_1:10;
hence x = [z,u]`1 by A23,A24,MCART_1:7
.= z by MCART_1:7;
end;
end;
take wwY; thus thesis by A10,A14,A21;
end;
hence thesis by A1,CARD_1:81;
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;
assume A1: v in (the carrier of g);
reconsider VV=the carrier of g as finite set by Th27; take VV;
consider ww being finite set such that A2:
ww={w where w is Element of X : w in VV & {v,w} in the SEdges of g} &
degree(g,v)=card ww by Th39;
A3: ww c= VV proof let e be set; assume e in ww;
then consider w being Element of X such that A4:
e=w & w in VV & {v,w} in (the SEdges of g) by A2; thus e in VV by A4;
end;
now assume ww=VV; then consider w being Element of X such that A5:
v=w & w in VV & {v,w} in (the SEdges of g) by A1,A2;
{v,v}={v} by ENUMSET1:69;
then consider x,y being set such that
A6: x in VV & y in VV & x<>y & {v}={x,y} by A5,Th10;
v=x & v=y by A6,ZFMISC_1:8;
hence ww<>VV by A6;
end;
then ww c< VV by A3,XBOOLE_0:def 8;
hence thesis by A2,CARD_2:67;
end;
theorem
for g being SimpleGraph of X, v,e being set st
v in the carrier of g & 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 A1:
v in the carrier of g & e in the SEdges of g & degree(g,v)=0;
assume A2: v in e;
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)) &
degree(g,v)=card(Y) by Def11;
Y is non empty by A1,A2,A3;
hence contradiction by A1,A3,CARD_2:59;
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 A1: vg=(the carrier of g) & v in vg & 1+degree(g,v)=(card vg);
then vg is Subset of X by Th27;
then reconsider X as non empty set by A1;
let w be Element of vg; assume A2: v<>w;
take {v,w};
hereby
now assume A3: not {v,w} in (the SEdges of g);
consider ww being finite set such that A4:
ww={vv where vv is Element of X :
vv in vg & {v,vv} in (the SEdges of g)} &
degree(g,v)=(card ww) by A1,Th39;
A5: now let e be set; assume e in ww;
then consider vv being Element of X such that A6:
e=vv & vv in vg & {v,vv} in (the SEdges of g) by A4;
thus e in vg by A6;
end;
A7: not v in ww & not w in ww proof
hereby assume v in ww;
then consider vv being Element of X such that A8:
v=vv & vv in vg & {v,vv} in (the SEdges of g) by A4;
{v} in (the SEdges of g) by A8,ENUMSET1:69;
then consider z being finite Element of (bool vg) such that A9:
({v}=z & (card z)=2) by A1,Th9;
thus contradiction by A9,CARD_1:79;
end;
assume w in ww;
then consider vv being Element of X such that A10:
w=vv & vv in vg & {v,vv} in (the SEdges of g) by A4;
thus contradiction by A3,A10;
end;
reconsider wwv=(ww \/ {v}) as finite set;
A11: (card wwv) = 1+(card ww) by A7,CARD_2:54;
wwv c= vg & wwv<>vg proof
A12: ww c= vg by A5,TARSKI:def 3;
for e being set st e in {v} holds e in vg by A1,TARSKI:def 1;
then {v} c= vg by TARSKI:def 3;
hence wwv c= vg by A12,XBOOLE_1:8;
A13: not w in {v} by A2,TARSKI:def 1;
assume wwv=vg; hence contradiction by A7,A13,XBOOLE_0:def 2;
end;
then wwv c< vg by XBOOLE_0:def 8;
hence contradiction by A1,A4,A11,CARD_2:67;
end;
hence {v,w} in the SEdges of g;
end;
thus {v,w}={v,w};
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 :Def12:
(p.1)=v1 & (p.(len p))=v2 &
(for i being Nat st (1<=i & i<(len p)) holds
{p.i, p.(i+1)} in (the SEdges of g)) &
(for i,j being Nat st 1<=i & i<(len p) & i<j & j<(len p) holds
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 :Def13:
{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 set; assume e in IT;
then consider ss being Element of (the carrier of g)* such that
A1: (e=ss & ss is_path_of v1,v2);
thus e in ((the carrier of g)*) by A1;
end;
hence IT is Subset of ((the carrier of g)*);
end;
end;
canceled;
theorem Th44: 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)))
proof let g be SimpleGraph of X, v1,v2 be Element of (the carrier of g),
e be set;
now assume e in PATHS(v1,v2);
then e in {ss where ss is Element of (the carrier of g)* :
ss is_path_of v1,v2} by Def13;
then consider ss being Element of (the carrier of g)* such that
A1: e = ss & ss is_path_of v1,v2;
take ss; thus e=ss & ss is_path_of v1,v2 by A1;
end;
hence e in PATHS(v1,v2) implies
(ex ss being Element of (the carrier of g)* st
(e=ss & ss is_path_of v1,v2));
assume ex ss being Element of (the carrier of g)* st
(ss=e & ss is_path_of v1,v2);
then e in {ss where ss is Element of (the carrier of g)* :
ss is_path_of v1,v2};
hence e in PATHS(v1,v2) by Def13;
end;
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) by Th44;
::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 :Def14:
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 Nat;
canceled;
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) & 1<=(m+1) by NAT_1:29;
then A1: V1 c= VV & V2 c= VV by Th5,FINSEQ_1:7;
A2: EE c= TWOELEMENTSETS(VV) proof let e be set; assume e in EE;
then consider i0,j0 being Element of NAT such that
A3: (e = {i0,j0} & i0 in V1 & j0 in V2);
A4: i0 in VV & j0 in VV & i0<>j0 & e={i0,j0} proof
thus i0 in VV & j0 in VV by A1,A3;
m<m+1 by NAT_1:38;
then V1 misses V2 by Th6;
then (V1 /\ V2) = {} by XBOOLE_0:def 7;
hence i0<>j0 & e={i0,j0} by A3,XBOOLE_0:def 3;
end;
e c= VV proof
for e0 being set st e0 in e holds e0 in VV by A4,TARSKI:def 2;
hence thesis by TARSKI:def 3; end;
hence e in TWOELEMENTSETS(VV) by A4,Th10;
end;
TWOELEMENTSETS(Seg (m+n)) is finite by Th15;
then reconsider EE as finite Subset of TWOELEMENTSETS(VV) by A2,FINSET_1:
13;
set IT = SimpleGraphStruct (# VV, EE #);
IT in SIMPLEGRAPHS(NAT) by Th21;
then reconsider IT as SimpleGraph of NAT by Def7;
reconsider EE as Subset of TWOELEMENTSETS(Seg (m+n));
take IT,EE; thus thesis;
end;
uniqueness;
end;
definition let n be Nat;
func K_(n) -> SimpleGraph of NAT means :Def17:
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};
A1: EE c= TWOELEMENTSETS(Seg n) proof
now let e be set; assume e in EE;
then consider i0,j0 being Element of NAT such that
A2: (e={i0,j0} & i0 in Seg n & j0 in Seg n & i0<>j0);
e c= (Seg n) proof let e0 be set; assume A3: e0 in e;
per cases by A2,A3,TARSKI:def 2;
suppose e0 = i0; hence e0 in Seg n by A2;
suppose e0 = j0; hence e0 in Seg n by A2;
end;
hence e in TWOELEMENTSETS(Seg n) by A2,Th10;
end;
hence thesis by TARSKI:def 3;
end;
TWOELEMENTSETS(Seg n) is finite by Th15;
then reconsider EE as finite Subset of TWOELEMENTSETS(Seg n)
by A1,FINSET_1:13;
set IT = SimpleGraphStruct (# Seg n,EE #);
IT in SIMPLEGRAPHS(NAT) by Th21;
then reconsider IT as SimpleGraph of NAT by Def7;
take IT,EE;
thus 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 #);
end;
uniqueness;
end;
:: TriangleGraph will be used in the definition of planegraphs.
definition
func TriangleGraph -> SimpleGraph of NAT equals :Def18:
K_(3);
correctness;
end;
theorem Th46: 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 Nat : i in (Seg 3) & j in (Seg 3) & i<>j} &
TriangleGraph = SimpleGraphStruct (#(Seg 3),ee#) by Def17,Def18;
take ee;
now let a be set; assume a in ee;
then consider i,j being Nat such that A2:
a={i,j}& i in (Seg 3) & j in (Seg 3) & i<>j by A1; per cases by A2,
ENUMSET1:def 1,FINSEQ_3:1;
suppose A3: i=1;
now per cases by A2,ENUMSET1:def 1,FINSEQ_3:1;
suppose j=1; hence a in {{1,2},{2,3},{3,1}} by A2,A3;
suppose j=2;
hence a in {{1,2},{2,3},{3,1}} by A2,A3,ENUMSET1:def 1;
suppose j=3;
hence a in {{1,2},{2,3},{3,1}} by A2,A3,ENUMSET1:def 1;
end;
hence a in {{1,2},{2,3},{3,1}};
suppose A4: i=2;
now per cases by A2,ENUMSET1:def 1,FINSEQ_3:1;
suppose j=1;
hence a in {{1,2},{2,3},{3,1}} by A2,A4,ENUMSET1:def 1;
suppose j=2; hence a in {{1,2},{2,3},{3,1}} by A2,A4;
suppose j=3;
hence a in {{1,2},{2,3},{3,1}} by A2,A4,ENUMSET1:def 1;
end;
hence a in {{1,2},{2,3},{3,1}};
suppose A5: i=3;
now per cases by A2,ENUMSET1:def 1,FINSEQ_3:1;
suppose j=1;
hence a in {{1,2},{2,3},{3,1}} by A2,A5,ENUMSET1:def 1;
suppose j=2;
hence a in {{1,2},{2,3},{3,1}} by A2,A5,ENUMSET1:def 1;
suppose j=3; hence a in {{1,2},{2,3},{3,1}} by A2,A5;
end;
hence a in {{1,2},{2,3},{3,1}};
end;
then A6: ee c= {{1,2},{2,3},{3,1}} by TARSKI:def 3;
now let e be set; assume A7: e in {{1,2},{2,3},{3,1}};
per cases by A7,ENUMSET1:def 1;
suppose A8: e={1,2};
now take i=1,j=2;
thus e={i,j} by A8;
thus i in Seg 3 & j in (Seg 3) by ENUMSET1:def 1,FINSEQ_3:1;
thus i<>j;
end;
hence e in ee by A1;
suppose A9: e={2,3};
now take i=2,j=3;
thus e={i,j} & i in (Seg 3) & j in (Seg 3) & i<>j
by A9,ENUMSET1:def 1,FINSEQ_3:1;
end;
hence e in ee by A1;
suppose A10: e={3,1};
now take i=3,j=1; thus
e={i,j} & i in (Seg 3) & j in (Seg 3) & i<>j
by A10,ENUMSET1:def 1,FINSEQ_3:1;
end;
hence e in ee by A1;
end;
then {{1,2},{2,3},{3,1}} c= ee by TARSKI:def 3;
hence thesis by A1,A6,XBOOLE_0:def 10;
end;
theorem (the carrier of TriangleGraph)=(Seg 3) &
(the SEdges of TriangleGraph) = {{1,2},{2,3},{3,1}} by Th46;
theorem
{1,2} in (the SEdges of TriangleGraph) &
{2,3} in (the SEdges of TriangleGraph) &
{3,1} in (the SEdges of TriangleGraph) by Th46,ENUMSET1:14;
theorem
<*1*>^<*2*>^<*3*>^<*1*> is_cycle_of TriangleGraph
proof
set p = <*1*>^<*2*>^<*3*>^<*1*>;
A1: (len p) = 4 & p.1 = 1 & p.2 = 2 & p.3 = 3 & p.4 = 1 by SCM_1:8;
reconsider VERTICES = (the carrier of TriangleGraph)
as non empty set by Th46,FINSEQ_1:3;
reconsider One=1, Two=2, Three=3 as Element of VERTICES by Th46,ENUMSET1:14,
FINSEQ_3:1;
reconsider one=1
as Element of (the carrier of TriangleGraph) by Th46,ENUMSET1:14,FINSEQ_3:1;
reconsider ONE=<*One*>, TWO=<*Two*>, THREE=<*Three*>
as FinSequence of (the carrier of TriangleGraph);
p = ONE^TWO^THREE^ONE &
ONE^TWO^THREE is FinSequence of (the carrier of TriangleGraph);
then reconsider pp=p as Element of (the carrier of TriangleGraph)* by
FINSEQ_1:def 11;
A2: now let i be Nat; assume (1<=i & i<(len p));
then 1<=i &i<3+1 by SCM_1:8; then 1<=i & i<=3 by NAT_1:38;
then A3: i in Seg 3 by FINSEQ_1:3;
per cases by A3,ENUMSET1:13,FINSEQ_3:1;
suppose i=1; hence {pp.i, pp.(i+1)} in (the SEdges of
TriangleGraph)
by A1,Th46,ENUMSET1:14;
suppose i=2; hence {pp.i, pp.(i+1)} in (the SEdges of TriangleGraph
)
by A1,Th46,ENUMSET1:14;
suppose i=3; hence {pp.i, pp.(i+1)} in (the SEdges of TriangleGraph
)
by A1,Th46,ENUMSET1:14;
end;
now let i,j be Nat; assume 1<=i & i<(len pp) & i<j & j<(len pp);
then A4: 1<=i & i<(3+1) & i<j & j<(3+1) by SCM_1:8;
then A5: 1<=i & i<=3 & i<j & j<=3 by NAT_1:38;
A6: 1<=(i+1) & (i+1)<=j & j<=3 by A4,NAT_1:38;
then A7: i in (Seg 3) & j in nat_interval(i+1,3)
by A5,Th2,FINSEQ_1:3;
per cases by A7,ENUMSET1:13,FINSEQ_3:1;
suppose A8: i=1; then A9: pp.i = one by SCM_1:8;
j=2 or (2<j & j<=3) by A6,A8,REAL_1:def 5;
then A10: j=2 or ((2+1)<=j & j<=3) by NAT_1:38;
now per cases by A10,AXIOMS:21;
suppose A11: j=2;
hence pp.i<>pp.j by A9,SCM_1:8;
thus {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)} by A1,A8,A11,ZFMISC_1:10
;
suppose A12: j=3;
hence pp.i<>pp.j by A9,SCM_1:8;
thus {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)} by A1,A8,A12,ZFMISC_1:10
;
end;
hence pp.i <> pp.j & {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)};
suppose A13: i=2;
then j=3 by A6,AXIOMS:21;
hence pp.i <> pp.j & {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)}
by A1,A13,ZFMISC_1:10;
suppose i=3;
hence pp.i <> pp.j & {pp.i,pp.(i+1)}<>{pp.j,pp.(j+1)} by A4,NAT_1:
38;
end;
then pp is_path_of one,one by A1,A2,Def12;
then pp in PATHS(one,one) by Th44;
hence thesis by Def14;
end;