:: The Formalisation of Simple Graphs
:: by Yozo Toda
::
:: Received September 8, 1994
:: Copyright (c) 1994-2026 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;
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<m holds Seg k misses nat_interval(m,n)
proof
let k,m,n be Nat;
assume
A1: k<m;
now
let e be object;
assume
A2: e in ((Seg k) /\ nat_interval(m,n));
then e in nat_interval(m,n) by XBOOLE_0:def 4;
then
A3: ex j being Nat st e=j & m<=j & j<=n;
e in (Seg k) by A2,XBOOLE_0:def 4;
then ex i being Nat st e=i & 1<=i & i<=k;
hence e in {} by A1,A3,XXREAL_0:2;
end;
then ((Seg k) /\ nat_interval(m,n)) c= {};
then ((Seg k) /\ nat_interval(m,n)) = {};
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 object;
assume e in nat_interval(m,n);
then ex i being Nat st e=i & m<=i & i<=n;
hence contradiction by A1,XXREAL_0:2;
end;
hence thesis by XBOOLE_0:def 1;
end;
Lm1: for A being set, s being Subset of A, n being set st n in A holds s \/ {n
} is Subset of A
proof
let A be set, s be Subset of A, n be set;
assume
A1: n in A;
s \/ {n} c= A
proof
let m be object;
assume
A2: m in (s \/ {n});
now
per cases by A2,XBOOLE_0:def 3;
suppose
m in s;
hence thesis;
end;
suppose
m in {n};
hence thesis by A1,TARSKI:def 1;
end;
end;
hence thesis;
end;
hence thesis;
end;
definition
let A be set;
func TWOELEMENTSETS(A) -> set equals
{z where z is Subset of A : card z = 2};
coherence;
end;
theorem Th7:
for A, e be set holds e in TWOELEMENTSETS(A) iff
ex z being Subset of A st e = z & card z = 2;
theorem Th8:
for A, 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,e be set;
hereby
assume e in TWOELEMENTSETS(A);
then
A1: ex z being 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;
let x be object;
assume x in TWOELEMENTSETS(A);
then x is finite Subset of A by Th8;
hence x in bool A;
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;
registration
cluster TWOELEMENTSETS {} -> empty;
coherence by Th11;
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;
::$CT 3
registration let A be finite set;
cluster TWOELEMENTSETS A -> finite;
coherence by Th9,FINSET_1:1;
end;
registration let A be non trivial set;
cluster TWOELEMENTSETS A -> non empty;
coherence
proof
consider a being object such that
A1: a in A by XBOOLE_0:def 1;
reconsider A9 = A as non empty non trivial set;
consider b being object such that
A2: b in (A9\{a}) by XBOOLE_0:def 1,ZFMISC_1:139;
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;
end;
registration let a be set;
cluster TWOELEMENTSETS {a} -> empty;
coherence
proof
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;
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;
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;
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,A15;
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;
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 A being set st A is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS(X) c= A
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 A being set st
A is_SetOfSimpleGraphs_of X holds SIMPLEGRAPHS(X) c= A 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 A3,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 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
A10: {v} c= vg by A2,TARSKI:def 1;
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<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
{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};
A1: V1 c= VV by FINSEQ_1:5,NAT_1:11;
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
A5: ee c= VV by A3,TARSKI:def 2;
m<m+1 by NAT_1:13;
then V1 /\ V2 = {} by XBOOLE_0:def 7,Th5;
then i0<>j0 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);
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);
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: i<len pp and
A12: i<j and
A13: j<len pp;
A14: (i+1)<=j by A12,NAT_1:13;
i<(3+1) by A11,FINSEQ_1:66;
then i<=3 by NAT_1:13;
then
A15: i in (Seg 3) by A10;
A16: j<(3+1) by A13,FINSEQ_1:66;
then
A17: j<=3 by NAT_1:13;
per cases by A15,ENUMSET1:def 1,FINSEQ_3:1;
suppose
A18: i=1;
then
A19: pp.i = o by FINSEQ_1:66;
j=2 or 2<j & j<=3 by A16,A14,A18,NAT_1:13,XXREAL_0:1;
then
A20: j=2 or (2+1)<=j & j<=3 by NAT_1:13;
now
per cases by A20,XXREAL_0:1;
suppose
A21: j=2;
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,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;
pp is_path_of o,o by A4,A5,A9,FINSEQ_1:66;
then pp in PATHS(o,o);
hence thesis;
end;