:: SGRAPH1 semantic presentation
begin
Lm1: for e being set
for n being Element of NAT st e in Seg n holds
ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
proof
let e be set ; ::_thesis: for n being Element of NAT st e in Seg n holds
ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
let n be Element of NAT ; ::_thesis: ( e in Seg n implies ex i being Element of NAT st
( e = i & 1 <= i & i <= n ) )
assume A1: e in Seg n ; ::_thesis: ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
then reconsider e = e as Element of NAT ;
take e ; ::_thesis: ( e = e & 1 <= e & e <= n )
thus ( e = e & 1 <= e & e <= n ) by A1, FINSEQ_1:1; ::_thesis: verum
end;
definition
let m, n be Nat;
func nat_interval (m,n) -> Subset of NAT equals :: SGRAPH1:def 1
{ i where i is Element of NAT : ( m <= i & i <= n ) } ;
coherence
{ i where i is Element of NAT : ( m <= i & i <= n ) } is Subset of NAT
proof
set IT = { i where i is Element of NAT : ( m <= i & i <= n ) } ;
now__::_thesis:_for_e_being_set_st_e_in__{__i_where_i_is_Element_of_NAT_:_(_m_<=_i_&_i_<=_n_)__}__holds_
e_in_{0}_\/_(Seg_n)
let e be set ; ::_thesis: ( e in { i where i is Element of NAT : ( m <= i & i <= n ) } implies e in {0} \/ (Seg n) )
assume e in { i where i is Element of NAT : ( m <= i & i <= n ) } ; ::_thesis: e in {0} \/ (Seg n)
then consider i being Element of NAT such that
A1: i = e and
m <= i and
A2: i <= n ;
now__::_thesis:_e_in_{0}_\/_(Seg_n)
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: e in {0} \/ (Seg n)
then i in {0} by TARSKI:def_1;
hence e in {0} \/ (Seg n) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: e in {0} \/ (Seg n)
then 0 + 1 <= i by NAT_1:13;
then e in Seg n by A1, A2, FINSEQ_1:1;
hence e in {0} \/ (Seg n) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence e in {0} \/ (Seg n) ; ::_thesis: verum
end;
then A3: { i where i is Element of NAT : ( m <= i & i <= n ) } c= {0} \/ (Seg n) by TARSKI:def_3;
{0} c= NAT by ZFMISC_1:31;
then {0} \/ (Seg n) c= NAT by XBOOLE_1:8;
hence { i where i is Element of NAT : ( m <= i & i <= n ) } is Subset of NAT by A3, XBOOLE_1:1; ::_thesis: verum
end;
end;
:: deftheorem defines nat_interval SGRAPH1:def_1_:_
for m, n being Nat holds nat_interval (m,n) = { i where i is Element of NAT : ( m <= i & i <= n ) } ;
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
nat_interval (m,n) is finite
proof
set IT = { i where i is Element of NAT : ( m <= i & i <= n ) } ;
now__::_thesis:_for_e_being_set_st_e_in__{__i_where_i_is_Element_of_NAT_:_(_m_<=_i_&_i_<=_n_)__}__holds_
e_in_{0}_\/_(Seg_n)
let e be set ; ::_thesis: ( e in { i where i is Element of NAT : ( m <= i & i <= n ) } implies e in {0} \/ (Seg n) )
assume e in { i where i is Element of NAT : ( m <= i & i <= n ) } ; ::_thesis: e in {0} \/ (Seg n)
then consider i being Element of NAT such that
A1: i = e and
m <= i and
A2: i <= n ;
now__::_thesis:_e_in_{0}_\/_(Seg_n)
percases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; ::_thesis: e in {0} \/ (Seg n)
then i in {0} by TARSKI:def_1;
hence e in {0} \/ (Seg n) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose i <> 0 ; ::_thesis: e in {0} \/ (Seg n)
then 0 + 1 <= i by NAT_1:13;
then e in Seg n by A1, A2, FINSEQ_1:1;
hence e in {0} \/ (Seg n) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence e in {0} \/ (Seg n) ; ::_thesis: verum
end;
then { i where i is Element of NAT : ( m <= i & i <= n ) } c= {0} \/ (Seg n) by TARSKI:def_3;
hence nat_interval (m,n) is finite ; ::_thesis: verum
end;
end;
theorem :: SGRAPH1:1
for m, n being Element of NAT
for e being set holds
( e in nat_interval (m,n) iff ex i being Element of NAT st
( e = i & m <= i & i <= n ) ) ;
theorem :: SGRAPH1:2
for m, n, k being Element of NAT holds
( k in nat_interval (m,n) iff ( m <= k & k <= n ) )
proof
let m, n, k be Element of NAT ; ::_thesis: ( k in nat_interval (m,n) iff ( m <= k & k <= n ) )
hereby ::_thesis: ( m <= k & k <= n implies k in nat_interval (m,n) )
assume k in nat_interval (m,n) ; ::_thesis: ( m <= k & k <= n )
then ex i being Element of NAT st
( k = i & m <= i & i <= n ) ;
hence ( m <= k & k <= n ) ; ::_thesis: verum
end;
assume ( m <= k & k <= n ) ; ::_thesis: k in nat_interval (m,n)
hence k in nat_interval (m,n) ; ::_thesis: verum
end;
theorem :: SGRAPH1:3
for n being Element of NAT holds nat_interval (1,n) = Seg n
proof
let n be Element of NAT ; ::_thesis: nat_interval (1,n) = Seg n
now__::_thesis:_for_e_being_set_st_e_in_Seg_n_holds_
e_in_nat_interval_(1,n)
let e be set ; ::_thesis: ( e in Seg n implies e in nat_interval (1,n) )
assume A1: e in Seg n ; ::_thesis: e in nat_interval (1,n)
then reconsider i = e as Element of NAT ;
( 1 <= i & i <= n ) by A1, FINSEQ_1:1;
hence e in nat_interval (1,n) ; ::_thesis: verum
end;
then A2: Seg n c= nat_interval (1,n) by TARSKI:def_3;
now__::_thesis:_for_e_being_set_st_e_in_nat_interval_(1,n)_holds_
e_in_Seg_n
let e be set ; ::_thesis: ( e in nat_interval (1,n) implies e in Seg n )
assume e in nat_interval (1,n) ; ::_thesis: e in Seg n
then ex i being Element of NAT st
( e = i & 1 <= i & i <= n ) ;
hence e in Seg n by FINSEQ_1:1; ::_thesis: verum
end;
then nat_interval (1,n) c= Seg n by TARSKI:def_3;
hence nat_interval (1,n) = Seg n by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th4: :: SGRAPH1:4
for m, n being Element of NAT st 1 <= m holds
nat_interval (m,n) c= Seg n
proof
let m, n be Element of NAT ; ::_thesis: ( 1 <= m implies nat_interval (m,n) c= Seg n )
assume A1: 1 <= m ; ::_thesis: nat_interval (m,n) c= Seg n
now__::_thesis:_for_e_being_set_st_e_in_nat_interval_(m,n)_holds_
e_in_Seg_n
let e be set ; ::_thesis: ( e in nat_interval (m,n) implies e in Seg n )
assume e in nat_interval (m,n) ; ::_thesis: e in Seg n
then consider i being Element of 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, FINSEQ_1:1; ::_thesis: verum
end;
hence nat_interval (m,n) c= Seg n by TARSKI:def_3; ::_thesis: verum
end;
theorem Th5: :: SGRAPH1:5
for k, m, n being Element of NAT st k < m holds
Seg k misses nat_interval (m,n)
proof
let k, m, n be Element of NAT ; ::_thesis: ( k < m implies Seg k misses nat_interval (m,n) )
assume A1: k < m ; ::_thesis: Seg k misses nat_interval (m,n)
now__::_thesis:_for_e_being_set_st_e_in_(Seg_k)_/\_(nat_interval_(m,n))_holds_
e_in_{}
let e be set ; ::_thesis: ( e in (Seg k) /\ (nat_interval (m,n)) implies e in {} )
assume A2: e in (Seg k) /\ (nat_interval (m,n)) ; ::_thesis: e in {}
then e in nat_interval (m,n) by XBOOLE_0:def_4;
then A3: ex j being Element of NAT st
( e = j & m <= j & j <= n ) ;
e in Seg k by A2, XBOOLE_0:def_4;
then ex i being Element of NAT st
( e = i & 1 <= i & i <= k ) by Lm1;
hence e in {} by A1, A3, XXREAL_0:2; ::_thesis: verum
end;
then (Seg k) /\ (nat_interval (m,n)) c= {} by TARSKI:def_3;
then (Seg k) /\ (nat_interval (m,n)) = {} ;
hence Seg k misses nat_interval (m,n) by XBOOLE_0:def_7; ::_thesis: verum
end;
theorem :: SGRAPH1:6
for m, n being Element of NAT st n < m holds
nat_interval (m,n) = {}
proof
let m, n be Element of NAT ; ::_thesis: ( n < m implies nat_interval (m,n) = {} )
assume A1: n < m ; ::_thesis: nat_interval (m,n) = {}
now__::_thesis:_for_e_being_set_holds_not_e_in_nat_interval_(m,n)
let e be set ; ::_thesis: not e in nat_interval (m,n)
assume e in nat_interval (m,n) ; ::_thesis: contradiction
then ex i being Element of NAT st
( e = i & m <= i & i <= n ) ;
hence contradiction by A1, XXREAL_0:2; ::_thesis: verum
end;
hence nat_interval (m,n) = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
Lm2: for A being set
for s being Subset of A
for n being set st n in A holds
s \/ {n} is Subset of A
proof
let A be set ; ::_thesis: for s being Subset of A
for n being set st n in A holds
s \/ {n} is Subset of A
let s be Subset of A; ::_thesis: for n being set st n in A holds
s \/ {n} is Subset of A
let n be set ; ::_thesis: ( n in A implies s \/ {n} is Subset of A )
assume A1: n in A ; ::_thesis: s \/ {n} is Subset of A
s \/ {n} c= A
proof
let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in s \/ {n} or m in A )
assume A2: m in s \/ {n} ; ::_thesis: m in A
now__::_thesis:_m_in_A
percases ( m in s or m in {n} ) by A2, XBOOLE_0:def_3;
suppose m in s ; ::_thesis: m in A
hence m in A ; ::_thesis: verum
end;
suppose m in {n} ; ::_thesis: m in A
hence m in A by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence m in A ; ::_thesis: verum
end;
hence s \/ {n} is Subset of A ; ::_thesis: verum
end;
definition
let A be set ;
func TWOELEMENTSETS A -> set equals :: SGRAPH1:def 2
{ z where z is finite Subset of A : card z = 2 } ;
coherence
{ z where z is finite Subset of A : card z = 2 } is set ;
end;
:: deftheorem defines TWOELEMENTSETS SGRAPH1:def_2_:_
for A being set holds TWOELEMENTSETS A = { z where z is finite Subset of A : card z = 2 } ;
theorem Th7: :: SGRAPH1:7
for A, e being set holds
( e in TWOELEMENTSETS A iff ex z being finite Subset of A st
( e = z & card z = 2 ) ) ;
theorem Th8: :: SGRAPH1:8
for A, e being 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, e be set ; ::_thesis: ( 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} ) ) )
hereby ::_thesis: ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) implies e in TWOELEMENTSETS A )
assume e in TWOELEMENTSETS A ; ::_thesis: ( e is finite Subset of A & ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) )
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; ::_thesis: ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} )
consider x, y being set such that
A2: x <> y and
A3: e9 = {x,y} by A1, CARD_2:60;
take x = x; ::_thesis: ex y being set st
( x in A & y in A & x <> y & e = {x,y} )
take y = y; ::_thesis: ( x in A & y in A & x <> y & e = {x,y} )
( x in e9 & y in e9 ) by A3, TARSKI:def_2;
hence ( x in A & y in A ) ; ::_thesis: ( x <> y & e = {x,y} )
thus ( x <> y & e = {x,y} ) by A2, A3; ::_thesis: verum
end;
assume that
e is finite Subset of A and
A4: ex x, y being set st
( x in A & y in A & x <> y & e = {x,y} ) ; ::_thesis: e in TWOELEMENTSETS A
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 ; ::_thesis: ( e = xy & card xy = 2 )
thus e = xy by A7; ::_thesis: card xy = 2
thus card xy = 2 by A6, CARD_2:57; ::_thesis: verum
end;
hence e in TWOELEMENTSETS A ; ::_thesis: verum
end;
theorem Th9: :: SGRAPH1:9
for A being set holds TWOELEMENTSETS A c= bool A
proof
let A be set ; ::_thesis: TWOELEMENTSETS A c= bool A
now__::_thesis:_for_x_being_set_st_x_in_TWOELEMENTSETS_A_holds_
x_in_bool_A
let x be set ; ::_thesis: ( x in TWOELEMENTSETS A implies x in bool A )
assume x in TWOELEMENTSETS A ; ::_thesis: x in bool A
then x is finite Subset of A by Th8;
hence x in bool A ; ::_thesis: verum
end;
hence TWOELEMENTSETS A c= bool A by TARSKI:def_3; ::_thesis: verum
end;
theorem Th10: :: SGRAPH1:10
for A, e1, e2 being set st {e1,e2} in TWOELEMENTSETS A holds
( e1 in A & e2 in A & e1 <> e2 )
proof
let A be set ; ::_thesis: for e1, e2 being set st {e1,e2} in TWOELEMENTSETS A holds
( e1 in A & e2 in A & e1 <> e2 )
let e1, e2 be set ; ::_thesis: ( {e1,e2} in TWOELEMENTSETS A implies ( e1 in A & e2 in A & e1 <> e2 ) )
assume A1: {e1,e2} in TWOELEMENTSETS A ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
then consider x, y being set such that
A2: ( x in A & y in A & not x = y ) and
A3: {e1,e2} = {x,y} by Th8;
percases ( ( e1 = x & e2 = x ) or ( e1 = x & e2 = y ) or ( e1 = y & e2 = x ) or ( e1 = y & e2 = y ) ) by A3, ZFMISC_1:6;
suppose ( e1 = x & e2 = x ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
then {x} in TWOELEMENTSETS A by A1, ENUMSET1:29;
then ex x1, x2 being set st
( x1 in A & x2 in A & not x1 = x2 & {x} = {x1,x2} ) by Th8;
hence ( e1 in A & e2 in A & e1 <> e2 ) by ZFMISC_1:5; ::_thesis: verum
end;
suppose ( e1 = x & e2 = y ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
hence ( e1 in A & e2 in A & e1 <> e2 ) by A2; ::_thesis: verum
end;
suppose ( e1 = y & e2 = x ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
hence ( e1 in A & e2 in A & e1 <> e2 ) by A2; ::_thesis: verum
end;
suppose ( e1 = y & e2 = y ) ; ::_thesis: ( e1 in A & e2 in A & e1 <> e2 )
then {y} in TWOELEMENTSETS A by A1, ENUMSET1:29;
then ex x1, x2 being set st
( x1 in A & x2 in A & not x1 = x2 & {y} = {x1,x2} ) by Th8;
hence ( e1 in A & e2 in A & e1 <> e2 ) by ZFMISC_1:5; ::_thesis: verum
end;
end;
end;
theorem Th11: :: SGRAPH1:11
TWOELEMENTSETS {} = {}
proof
TWOELEMENTSETS {} c= {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in TWOELEMENTSETS {} or a in {} )
assume a in TWOELEMENTSETS {} ; ::_thesis: a in {}
then ex a1, a2 being set st
( a1 in {} & a2 in {} & not a1 = a2 & a = {a1,a2} ) by Th8;
hence a in {} ; ::_thesis: verum
end;
hence TWOELEMENTSETS {} = {} ; ::_thesis: verum
end;
theorem :: SGRAPH1:12
for t, u being set st t c= u holds
TWOELEMENTSETS t c= TWOELEMENTSETS u
proof
let t, u be set ; ::_thesis: ( t c= u implies TWOELEMENTSETS t c= TWOELEMENTSETS u )
assume A1: t c= u ; ::_thesis: TWOELEMENTSETS t c= TWOELEMENTSETS u
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in TWOELEMENTSETS t or e in TWOELEMENTSETS u )
assume A2: e in TWOELEMENTSETS t ; ::_thesis: e in TWOELEMENTSETS u
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 set st
( x in t & y in t & not x = y & e = {x,y} ) by A2, Th8;
hence e in TWOELEMENTSETS u by A1, A3, Th8; ::_thesis: verum
end;
theorem Th13: :: SGRAPH1:13
for A being finite set holds TWOELEMENTSETS A is finite by Th9, FINSET_1:1;
theorem :: SGRAPH1:14
for A being non trivial set holds not TWOELEMENTSETS A is empty
proof
let A be non trivial set ; ::_thesis: not TWOELEMENTSETS A is empty
consider a being set 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 REALSET1:3;
then consider b being set 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 not TWOELEMENTSETS A is empty by A1, A2, A3, Th8; ::_thesis: verum
end;
theorem :: SGRAPH1:15
for a being set holds TWOELEMENTSETS {a} = {}
proof
let a be set ; ::_thesis: TWOELEMENTSETS {a} = {}
now__::_thesis:_for_x_being_set_holds_not_x_in_TWOELEMENTSETS_{a}
let x be set ; ::_thesis: not x in TWOELEMENTSETS {a}
assume x in TWOELEMENTSETS {a} ; ::_thesis: contradiction
then consider u, v being set 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; ::_thesis: verum
end;
hence TWOELEMENTSETS {a} = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
begin
definition
attrc1 is strict ;
struct SimpleGraphStruct -> 1-sorted ;
aggrSimpleGraphStruct(# carrier, SEdges #) -> SimpleGraphStruct ;
sel SEdges c1 -> Subset of (TWOELEMENTSETS the carrier of c1);
end;
definition
let X be set ;
func SIMPLEGRAPHS X -> set equals :: SGRAPH1:def 3
{ SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } ;
coherence
{ SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } is set ;
end;
:: deftheorem defines SIMPLEGRAPHS SGRAPH1:def_3_:_
for X being set holds SIMPLEGRAPHS X = { SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } ;
theorem Th16: :: SGRAPH1:16
for X being set holds SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X
proof
let X be set ; ::_thesis: SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X
reconsider phiv = {} as finite Subset of 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) : verum } ;
hence SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X ; ::_thesis: verum
end;
registration
let X be set ;
cluster SIMPLEGRAPHS X -> non empty ;
coherence
not SIMPLEGRAPHS X is empty by Th16;
end;
definition
let X be set ;
mode SimpleGraph of X -> strict SimpleGraphStruct means :Def4: :: SGRAPH1:def 4
it is Element of SIMPLEGRAPHS X;
existence
ex b1 being strict SimpleGraphStruct st b1 is Element of SIMPLEGRAPHS X
proof
take SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) ; ::_thesis: SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) is Element of SIMPLEGRAPHS X
thus SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) is Element of SIMPLEGRAPHS X by Th16; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines SimpleGraph SGRAPH1:def_4_:_
for X being set
for b2 being strict SimpleGraphStruct holds
( b2 is SimpleGraph of X iff b2 is Element of SIMPLEGRAPHS X );
theorem Th17: :: SGRAPH1:17
for X, g being set holds
( g in SIMPLEGRAPHS X iff ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) ) ;
begin
theorem Th18: :: SGRAPH1:18
for X being set
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 X be set ; ::_thesis: for g being SimpleGraph of X holds
( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )
let g be SimpleGraph of X; ::_thesis: ( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )
g is Element of SIMPLEGRAPHS X by Def4;
then ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) by Th17;
hence the carrier of g c= X ; ::_thesis: the SEdges of g c= TWOELEMENTSETS the carrier of g
thus the SEdges of g c= TWOELEMENTSETS the carrier of g ; ::_thesis: verum
end;
theorem :: SGRAPH1:19
for X being set
for g being SimpleGraph of X
for 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 Th8;
theorem :: SGRAPH1:20
for X being set
for g being SimpleGraph of X
for 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: :: SGRAPH1:21
for X being set
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 X be set ; ::_thesis: 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) )
let g be SimpleGraph of X; ::_thesis: ( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) )
g is Element of SIMPLEGRAPHS X by Def4;
then ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) by Th17;
hence ( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) ) ; ::_thesis: verum
end;
definition
let X be set ;
let G, G9 be SimpleGraph of X;
predG is_isomorphic_to G9 means :: SGRAPH1:def 5
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;
:: deftheorem defines is_isomorphic_to SGRAPH1:def_5_:_
for X being set
for G, G9 being SimpleGraph of X holds
( G is_isomorphic_to G9 iff 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 ) ) ) );
begin
scheme :: SGRAPH1:sch 1
IndSimpleGraphs0{ F1() -> set , P1[ set ] } :
for G being set st G in SIMPLEGRAPHS F1() holds
P1[G]
provided
A1: P1[ SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #)] and
A2: for g being SimpleGraph of F1()
for v being set st g in SIMPLEGRAPHS F1() & P1[g] & v in F1() & not v in the carrier of g holds
P1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)] and
A3: for g being SimpleGraph of F1()
for e being set st P1[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} & P1[ SimpleGraphStruct(# the carrier of g,sege #)] )
proof
let g be set ; ::_thesis: ( g in SIMPLEGRAPHS F1() implies P1[g] )
assume A4: g in SIMPLEGRAPHS F1() ; ::_thesis: P1[g]
then A5: ex v being finite Subset of F1() ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) ;
then reconsider G = g as SimpleGraph of F1() by A4, Def4;
A6: the carrier of G c= F1() by Th18;
percases ( F1() is empty or not F1() is empty ) ;
supposeA7: F1() is empty ; ::_thesis: P1[g]
then the SEdges of G is Subset of {} by A6, Th11;
hence P1[g] by A1, A6, A7; ::_thesis: verum
end;
suppose not F1() is empty ; ::_thesis: P1[g]
then reconsider X = F1() as non empty set ;
defpred S1[ set ] means P1[ SimpleGraphStruct(# $1,({} (TWOELEMENTSETS $1)) #)];
A8: now__::_thesis:_for_B9_being_Element_of_Fin_X
for_b_being_Element_of_X_st_S1[B9]_&_not_b_in_B9_holds_
S1[B9_\/_{b}]
let B9 be Element of Fin X; ::_thesis: for b being Element of X st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let b be Element of X; ::_thesis: ( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
set g = SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #);
B9 is finite Subset of X by FINSUB_1:17;
then A9: SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #) in SIMPLEGRAPHS F1() ;
then reconsider g = SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #) as SimpleGraph of F1() by Def4;
assume ( S1[B9] & not b in B9 ) ; ::_thesis: S1[B9 \/ {b}]
then P1[ SimpleGraphStruct(# ( the carrier of g \/ {b}),({} (TWOELEMENTSETS ( the carrier of g \/ {b}))) #)] by A2, A9;
hence S1[B9 \/ {b}] ; ::_thesis: verum
end;
A10: S1[ {}. X] by A1;
A11: for VV being Element of Fin X holds S1[VV] from SETWISEO:sch_2(A10, A8);
A12: now__::_thesis:_for_VV_being_Element_of_Fin_X
for_EEa_being_Finite_Subset_of_(TWOELEMENTSETS_VV)
for_EE_being_Subset_of_(TWOELEMENTSETS_VV)_st_EEa_=_EE_holds_
P1[_SimpleGraphStruct(#_VV,EE_#)]
let VV be Element of Fin X; ::_thesis: for EEa being Finite_Subset of (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b3 holds
P1[ SimpleGraphStruct(# EEa,b3 #)]
percases ( TWOELEMENTSETS VV = {} or TWOELEMENTSETS VV <> {} ) ;
supposeA13: TWOELEMENTSETS VV = {} ; ::_thesis: for EEa being Finite_Subset of (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b3 holds
P1[ SimpleGraphStruct(# EEa,b3 #)]
let EEa be Finite_Subset of (TWOELEMENTSETS VV); ::_thesis: for EE being Subset of (TWOELEMENTSETS VV) st EEa = EE holds
P1[ SimpleGraphStruct(# VV,EE #)]
let EE be Subset of (TWOELEMENTSETS VV); ::_thesis: ( EEa = EE implies P1[ SimpleGraphStruct(# VV,EE #)] )
assume EEa = EE ; ::_thesis: P1[ SimpleGraphStruct(# VV,EE #)]
EE = {} (TWOELEMENTSETS VV) by A13;
hence P1[ SimpleGraphStruct(# VV,EE #)] by A11; ::_thesis: verum
end;
suppose TWOELEMENTSETS VV <> {} ; ::_thesis: for EE being Finite_Subset of (TWOELEMENTSETS EE)
for EE9 being Subset of (TWOELEMENTSETS EE) st b3 = EE9 holds
P1[ SimpleGraphStruct(# EE,b3 #)]
then reconsider TT = TWOELEMENTSETS VV as non empty set ;
defpred S2[ Finite_Subset of TT] means for EE being Subset of (TWOELEMENTSETS VV) st EE = $1 holds
P1[ SimpleGraphStruct(# VV,EE #)];
A14: now__::_thesis:_for_ee_being_Finite_Subset_of_TT
for_vv_being_Element_of_TT_st_S2[ee]_&_not_vv_in_ee_holds_
S2[ee_\/_{.vv.}]
let ee be Finite_Subset of TT; ::_thesis: for vv being Element of TT st S2[ee] & not vv in ee holds
S2[ee \/ {.vv.}]
let vv be Element of TT; ::_thesis: ( S2[ee] & not vv in ee implies S2[ee \/ {.vv.}] )
assume that
A15: S2[ee] and
A16: not vv in ee ; ::_thesis: S2[ee \/ {.vv.}]
reconsider ee9 = ee as Subset of (TWOELEMENTSETS VV) by FINSUB_1:17;
set g = SimpleGraphStruct(# VV,ee9 #);
VV is finite Subset of F1() by FINSUB_1:17;
then SimpleGraphStruct(# VV,ee9 #) is Element of SIMPLEGRAPHS F1() by Th17;
then reconsider g = SimpleGraphStruct(# VV,ee9 #) as SimpleGraph of F1() by Def4;
P1[g] by A15;
then ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {vv} & P1[ SimpleGraphStruct(# the carrier of g,sege #)] ) by A3, A16;
hence S2[ee \/ {.vv.}] ; ::_thesis: verum
end;
A17: S2[ {}. TT]
proof
let EE be Subset of (TWOELEMENTSETS VV); ::_thesis: ( EE = {}. TT implies P1[ SimpleGraphStruct(# VV,EE #)] )
assume EE = {}. TT ; ::_thesis: P1[ SimpleGraphStruct(# VV,EE #)]
then EE = {} (TWOELEMENTSETS VV) ;
hence P1[ SimpleGraphStruct(# VV,EE #)] by A11; ::_thesis: verum
end;
for EE being Finite_Subset of TT holds S2[EE] from SETWISEO:sch_2(A17, A14);
hence for EE being Finite_Subset of (TWOELEMENTSETS VV)
for EE9 being Subset of (TWOELEMENTSETS VV) st EE9 = EE holds
P1[ SimpleGraphStruct(# VV,EE9 #)] ; ::_thesis: verum
end;
end;
end;
( the carrier of G is Finite_Subset of X & the SEdges of G is Finite_Subset of (TWOELEMENTSETS the carrier of G) ) by A5, FINSUB_1:def_5;
hence P1[g] by A12; ::_thesis: verum
end;
end;
end;
theorem :: SGRAPH1:22
for X being set
for g being SimpleGraph of X holds
( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) ) )
proof
let X be set ; ::_thesis: for g being SimpleGraph of X holds
( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) ) )
let g be SimpleGraph of X; ::_thesis: ( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) ) )
assume A1: not g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) ; ::_thesis: ex v being set ex e being Subset of (TWOELEMENTSETS v) st
( not v is empty & g = SimpleGraphStruct(# v,e #) )
take the carrier of g ; ::_thesis: ex e being Subset of (TWOELEMENTSETS the carrier of g) st
( not the carrier of g is empty & g = SimpleGraphStruct(# the carrier of g,e #) )
take the SEdges of g ; ::_thesis: ( not the carrier of g is empty & g = SimpleGraphStruct(# the carrier of g, the SEdges of g #) )
thus not the carrier of g is empty by A1, Th11; ::_thesis: g = SimpleGraphStruct(# the carrier of g, the SEdges of g #)
thus g = SimpleGraphStruct(# the carrier of g, the SEdges of g #) ; ::_thesis: verum
end;
theorem Th23: :: SGRAPH1:23
for X being set
for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for 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 X be set ; ::_thesis: for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for 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
let V be Subset of X; ::_thesis: for E being Subset of (TWOELEMENTSETS V)
for n being set
for 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
let E be Subset of (TWOELEMENTSETS V); ::_thesis: for n being set
for 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
let n be set ; ::_thesis: for 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
let Evn be finite Subset of (TWOELEMENTSETS (V \/ {n})); ::_thesis: ( SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X implies SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X )
set g = SimpleGraphStruct(# V,E #);
assume that
A1: SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X and
A2: n in X ; ::_thesis: SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X
reconsider g = SimpleGraphStruct(# V,E #) 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, Lm2;
hence SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X ; ::_thesis: verum
end;
theorem Th24: :: SGRAPH1:24
for X being set
for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for 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 X be set ; ::_thesis: for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for 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 )
let V be Subset of X; ::_thesis: for E being Subset of (TWOELEMENTSETS V)
for 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 )
let E be Subset of (TWOELEMENTSETS V); ::_thesis: for 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 )
let v1, v2 be set ; ::_thesis: ( v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X implies ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) )
set g = SimpleGraphStruct(# V,E #);
assume that
A1: ( v1 in V & v2 in V ) and
A2: not v1 = v2 and
A3: SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X ; ::_thesis: ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
reconsider g = SimpleGraphStruct(# V,E #) 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 = V as finite Subset of X ;
( E \/ {{v1,v2}} c= TWOELEMENTSETS V & E \/ {{v1,v2}} is finite )
proof
hereby :: according to TARSKI:def_3 ::_thesis: E \/ {{v1,v2}} is finite
let e be set ; ::_thesis: ( e in E \/ {{v1,v2}} implies b1 in TWOELEMENTSETS V )
assume A5: e in E \/ {{v1,v2}} ; ::_thesis: b1 in TWOELEMENTSETS V
percases ( e in E or e in {{v1,v2}} ) by A5, XBOOLE_0:def_3;
suppose e in E ; ::_thesis: b1 in TWOELEMENTSETS V
hence e in TWOELEMENTSETS V ; ::_thesis: verum
end;
suppose e in {{v1,v2}} ; ::_thesis: b1 in TWOELEMENTSETS V
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; ::_thesis: verum
end;
end;
end;
thus E \/ {{v1,v2}} is finite by A4; ::_thesis: verum
end;
then reconsider E9 = E \/ {{v1,v2}} as finite Subset of (TWOELEMENTSETS V) ;
SimpleGraphStruct(# V,E9 #) in SIMPLEGRAPHS X ;
hence ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) ; ::_thesis: verum
end;
definition
let X, GG be set ;
predGG is_SetOfSimpleGraphs_of X means :Def6: :: SGRAPH1:def 6
( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG & ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for 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
for E being Subset of (TWOELEMENTSETS V)
for 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;
:: deftheorem Def6 defines is_SetOfSimpleGraphs_of SGRAPH1:def_6_:_
for X, GG being set holds
( GG is_SetOfSimpleGraphs_of X iff ( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG & ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for 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
for E being Subset of (TWOELEMENTSETS V)
for 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 ) ) ) );
theorem Th25: :: SGRAPH1:25
for X being set holds SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X
proof
let X be set ; ::_thesis: SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X
thus SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in SIMPLEGRAPHS X by Th16; :: according to SGRAPH1:def_6 ::_thesis: ( ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for n being set
for 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 ) & ( for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for 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 ) ) )
thus for VV being Subset of X
for EE being Subset of (TWOELEMENTSETS VV)
for nn being set
for 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 Th23; ::_thesis: for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for 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 )
thus for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for 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 Th24; ::_thesis: verum
end;
theorem Th26: :: SGRAPH1:26
for X, OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS X c= OTHER
proof
let X, OTHER be set ; ::_thesis: ( OTHER is_SetOfSimpleGraphs_of X implies SIMPLEGRAPHS X c= OTHER )
defpred S1[ set ] means $1 in OTHER;
assume A1: OTHER is_SetOfSimpleGraphs_of X ; ::_thesis: SIMPLEGRAPHS X c= OTHER
A2: for g being SimpleGraph of X
for v being set st g in SIMPLEGRAPHS X & S1[g] & v in X & not v in the carrier of g holds
S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
proof
let g be SimpleGraph of X; ::_thesis: for v being set st g in SIMPLEGRAPHS X & S1[g] & v in X & not v in the carrier of g holds
S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
let v be set ; ::_thesis: ( g in SIMPLEGRAPHS X & S1[g] & v in X & not v in the carrier of g implies S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)] )
assume that
g in SIMPLEGRAPHS X and
A3: ( g in OTHER & v in X & not v in the carrier of g ) ; ::_thesis: S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
set SVg = the carrier of g;
the carrier of g is Subset of X by Th21;
hence S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)] by A1, A3, Def6; ::_thesis: verum
end;
A4: for g being SimpleGraph of X
for e being set st S1[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} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
proof
let g be SimpleGraph of X; ::_thesis: for e being set st S1[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} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
let e be set ; ::_thesis: ( S1[g] & e in TWOELEMENTSETS the carrier of g & not e in the SEdges of g implies ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] ) )
assume that
A5: g in OTHER and
A6: e in TWOELEMENTSETS the carrier of g and
A7: not e in the SEdges of g ; ::_thesis: ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
set SVg = the carrier of g;
set SEg = the SEdges of g;
consider v1, v2 being set such that
A8: ( v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 ) and
A9: e = {v1,v2} by A6, Th8;
the carrier of g is finite Subset of X by Th21;
then consider v1v2 being finite Subset of (TWOELEMENTSETS the carrier of g) such that
A10: ( v1v2 = the SEdges of g \/ {{v1,v2}} & SimpleGraphStruct(# the carrier of g,v1v2 #) in OTHER ) by A1, A5, A7, A8, A9, Def6;
take v1v2 ; ::_thesis: ( v1v2 = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,v1v2 #)] )
thus ( v1v2 = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,v1v2 #)] ) by A9, A10; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in SIMPLEGRAPHS X or e in OTHER )
assume A11: e in SIMPLEGRAPHS X ; ::_thesis: e in OTHER
A12: S1[ SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #)] by A1, Def6;
for e being set st e in SIMPLEGRAPHS X holds
S1[e] from SGRAPH1:sch_1(A12, A2, A4);
hence e in OTHER by A11; ::_thesis: verum
end;
theorem :: SGRAPH1:27
for X being set holds
( 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
definition
let X be set ;
let G be SimpleGraph of X;
mode SubGraph of G -> SimpleGraph of X means :: SGRAPH1:def 7
( the carrier of it c= the carrier of G & the SEdges of it c= the SEdges of G );
existence
ex b1 being SimpleGraph of X st
( the carrier of b1 c= the carrier of G & the SEdges of b1 c= the SEdges of G ) ;
end;
:: deftheorem defines SubGraph SGRAPH1:def_7_:_
for X being set
for G, b3 being SimpleGraph of X holds
( b3 is SubGraph of G iff ( the carrier of b3 c= the carrier of G & the SEdges of b3 c= the SEdges of G ) );
begin
definition
let X be set ;
let G be SimpleGraph of X;
let v be set ;
func degree (G,v) -> Element of NAT means :Def8: :: SGRAPH1:def 8
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
ex b1 being Element of NAT ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b1 = card X )
proof
defpred S1[ 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 & S1[z] ) ) from XBOOLE_0:sch_1();
A2: X c= the SEdges of G
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in the SEdges of G )
assume z in X ; ::_thesis: z in the SEdges of G
hence z in the SEdges of G by A1; ::_thesis: verum
end;
the SEdges of G is finite by Th21;
then reconsider X = X as finite set by A2;
take card X ; ::_thesis: ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X )
take X ; ::_thesis: ( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X )
thus ( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & card X = card X ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b1 = card X ) & ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b2 = card X ) holds
b1 = b2
proof
let IT1, IT2 be Element of NAT ; ::_thesis: ( ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & IT1 = card X ) & ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & IT2 = card X ) implies IT1 = IT2 )
assume ( ex X1 being 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 being finite set st
( ( for z being set holds
( z in X2 iff ( z in the SEdges of G & v in z ) ) ) & IT2 = card X2 ) ) ; ::_thesis: IT1 = IT2
then consider X1, X2 being 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X2 or z in X1 )
assume z in X2 ; ::_thesis: z in X1
then ( z in the SEdges of G & v in z ) by A5;
hence z in X1 by A3; ::_thesis: verum
end;
X1 c= X2
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X1 or z in X2 )
assume z in X1 ; ::_thesis: z in X2
then ( z in the SEdges of G & v in z ) by A3;
hence z in X2 by A5; ::_thesis: verum
end;
hence IT1 = IT2 by A4, A6, A7, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines degree SGRAPH1:def_8_:_
for X being set
for G being SimpleGraph of X
for v being set
for b4 being Element of NAT holds
( b4 = degree (G,v) iff ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & b4 = card X ) );
theorem Th28: :: SGRAPH1:28
for X being non empty set
for G being SimpleGraph of X
for v being set 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 ; ::_thesis: for G being SimpleGraph of X
for v being set 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 )
let G be SimpleGraph of X; ::_thesis: for v being set 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 )
let v be set ; ::_thesis: 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 )
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 { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } iff ( z in the carrier of G & {v,z} in the SEdges of G ) )
proof
let z be set ; ::_thesis: ( z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } iff ( z in the carrier of G & {v,z} in the SEdges of G ) )
hereby ::_thesis: ( z in the carrier of G & {v,z} in the SEdges of G implies z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } )
assume z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ; ::_thesis: ( z in the carrier of G & {v,z} in the SEdges of G )
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 ) ; ::_thesis: verum
end;
thus ( z in the carrier of G & {v,z} in the SEdges of G implies z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ) ::_thesis: verum
proof
assume A4: ( z in the carrier of G & {v,z} in the SEdges of G ) ; ::_thesis: z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) }
the carrier of G is finite Subset of X by Th21;
hence z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } by A4; ::_thesis: verum
end;
end;
A5: { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } c= the carrier of G
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } or z in the carrier of G )
assume z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ; ::_thesis: z in the carrier of G
hence z in the carrier of G by A3; ::_thesis: verum
end;
the carrier of G is finite by Th21;
then reconsider ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } as finite set by A5;
take ww ; ::_thesis: ( 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 )
ww,Y are_equipotent
proof
set wwY = { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ;
take { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; :: according to TARSKI:def_6 ::_thesis: ( ( for b1 being set holds
( not b1 in ww or ex b2 being set st
( b2 in Y & [b1,b2] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b1 being set holds
( not b1 in Y or ex b2 being set st
( b2 in ww & [b2,b1] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or not [b3,b4] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
A6: for x, y, z, u being set st [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } & [z,u] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } holds
( x = z iff y = u )
proof
let x, y, z, u be set ; ::_thesis: ( [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } & [z,u] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } implies ( x = z iff y = u ) )
assume that
A7: [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } and
A8: [z,u] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; ::_thesis: ( x = z iff y = u )
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 ::_thesis: ( y = u implies x = z )
assume A12: x = z ; ::_thesis: y = u
w1 = [x,y] `1 by A9, MCART_1:7
.= z by A12
.= [w2,{v,w2}] `1 by A11, MCART_1:7
.= w2 ;
hence y = [w2,{v,w2}] `2 by A9, MCART_1:7
.= u by A11, MCART_1:7 ;
::_thesis: verum
end;
hereby ::_thesis: verum
{v,w1} in the SEdges of G by A1, A10;
then A13: v <> w1 by Th10;
assume A14: y = u ; ::_thesis: x = z
{v,w1} = [x,y] `2 by A9, MCART_1:7
.= u by A14
.= [w2,{v,w2}] `2 by A11, MCART_1:7
.= {v,w2} ;
then w1 = w2 by A13, ZFMISC_1:6;
hence x = [z,u] `1 by A9, A11, MCART_1:7
.= z ;
::_thesis: verum
end;
end;
A15: for w being set holds
( [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } iff ( w in ww & {v,w} in Y ) )
proof
let w be set ; ::_thesis: ( [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } iff ( w in ww & {v,w} in Y ) )
hereby ::_thesis: ( w in ww & {v,w} in Y implies [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
assume [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; ::_thesis: ( w in ww & {v,w} in Y )
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, MCART_1:7
.= w9 ;
hence ( w in ww & {v,w} in Y ) by A17; ::_thesis: verum
end;
thus ( w in ww & {v,w} in Y implies [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ::_thesis: verum
proof
assume that
A18: w in ww and
A19: {v,w} in Y ; ::_thesis: [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {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 = 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 [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; ::_thesis: verum
end;
end;
A21: for y being set st y in Y holds
ex x being set st
( x in ww & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
proof
let y be set ; ::_thesis: ( y in Y implies ex x being set st
( x in ww & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) )
assume A22: y in Y ; ::_thesis: ex x being set st
( x in ww & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
then A23: y in the SEdges of G by A1;
A24: v in y by A1, A22;
ex w being set st
( w in the carrier of G & y = {v,w} )
proof
consider v1, v2 being set 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;
percases ( v = v1 or v = v2 ) by A24, A27, TARSKI:def_2;
supposeA28: v = v1 ; ::_thesis: ex w being set st
( w in the carrier of G & y = {v,w} )
take v2 ; ::_thesis: ( v2 in the carrier of G & y = {v,v2} )
thus ( v2 in the carrier of G & y = {v,v2} ) by A26, A27, A28; ::_thesis: verum
end;
supposeA29: v = v2 ; ::_thesis: ex w being set st
( w in the carrier of G & y = {v,w} )
take v1 ; ::_thesis: ( v1 in the carrier of G & y = {v,v1} )
thus v1 in the carrier of G by A25; ::_thesis: y = {v,v1}
thus y = {v,v1} by A27, A29; ::_thesis: verum
end;
end;
end;
then consider w being set such that
A30: w in the carrier of G and
A31: y = {v,w} ;
take w ; ::_thesis: ( w in ww & [w,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
thus w in ww by A3, A23, A30, A31; ::_thesis: [w,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) }
hence [w,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } by A15, A22, A31; ::_thesis: verum
end;
for x being set st x in ww holds
ex y being set st
( y in Y & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
proof
let x be set ; ::_thesis: ( x in ww implies ex y being set st
( y in Y & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) )
assume A32: x in ww ; ::_thesis: ex y being set st
( y in Y & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
take {v,x} ; ::_thesis: ( {v,x} in Y & [x,{v,x}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
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; ::_thesis: [x,{v,x}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) }
hence [x,{v,x}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } by A15, A32; ::_thesis: verum
end;
hence ( ( for b1 being set holds
( not b1 in ww or ex b2 being set st
( b2 in Y & [b1,b2] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b1 being set holds
( not b1 in Y or ex b2 being set st
( b2 in ww & [b2,b1] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or not [b3,b4] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) ) by A21, A6; ::_thesis: verum
end;
hence ( 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 ) by A2, CARD_1:5; ::_thesis: verum
end;
theorem :: SGRAPH1:29
for X being non empty set
for g being SimpleGraph of X
for 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 ; ::_thesis: for g being SimpleGraph of X
for 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 )
let g be SimpleGraph of X; ::_thesis: for 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 )
let v be set ; ::_thesis: ( v in the carrier of g implies ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV ) )
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 ; ::_thesis: ex VV being finite set st
( VV = the carrier of g & degree (g,v) < card VV )
A4: now__::_thesis:_(_ww_=_VV_implies_ww_<>_VV_)
assume ww = VV ; ::_thesis: 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 set 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; ::_thesis: verum
end;
take VV ; ::_thesis: ( VV = the carrier of g & degree (g,v) < card VV )
ww c= VV
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ww or e in VV )
assume e in ww ; ::_thesis: e in VV
then ex w being Element of X st
( e = w & w in VV & {v,w} in the SEdges of g ) by A1;
hence e in VV ; ::_thesis: verum
end;
then ww c< VV by A4, XBOOLE_0:def_8;
hence ( VV = the carrier of g & degree (g,v) < card VV ) by A2, CARD_2:48; ::_thesis: verum
end;
theorem :: SGRAPH1:30
for X being set
for g being SimpleGraph of X
for v, e being set st e in the SEdges of g & degree (g,v) = 0 holds
not v in e
proof
let X be set ; ::_thesis: for g being SimpleGraph of X
for v, e being set st e in the SEdges of g & degree (g,v) = 0 holds
not v in e
let g be SimpleGraph of X; ::_thesis: for v, e being set st e in the SEdges of g & degree (g,v) = 0 holds
not v in e
let v, e be set ; ::_thesis: ( e in the SEdges of g & degree (g,v) = 0 implies not v in e )
assume that
A1: e in the SEdges of g and
A2: degree (g,v) = 0 ; ::_thesis: not v in e
consider Y being 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 ; ::_thesis: contradiction
then not Y is empty by A1, A3;
hence contradiction by A2, A4; ::_thesis: verum
end;
theorem :: SGRAPH1:31
for X being set
for g being SimpleGraph of X
for v being set
for 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 X be set ; ::_thesis: for g being SimpleGraph of X
for v being set
for 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} )
let g be SimpleGraph of X; ::_thesis: for v being set
for 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} )
let v be set ; ::_thesis: for 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} )
let vg be finite set ; ::_thesis: ( vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg implies for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} ) )
assume that
A1: vg = the carrier of g and
A2: v in vg and
A3: 1 + (degree (g,v)) = card vg ; ::_thesis: for w being Element of vg st v <> w holds
ex e being set st
( e in the SEdges of g & e = {v,w} )
vg is Subset of X by A1, Th21;
then reconsider X = X as non empty set by A2;
let w be Element of vg; ::_thesis: ( v <> w implies ex e being set st
( e in the SEdges of g & e = {v,w} ) )
assume A4: v <> w ; ::_thesis: ex e being set st
( e in the SEdges of g & e = {v,w} )
take {v,w} ; ::_thesis: ( {v,w} in the SEdges of g & {v,w} = {v,w} )
hereby ::_thesis: {v,w} = {v,w}
now__::_thesis:_{v,w}_in_the_SEdges_of_g
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 ; ::_thesis: contradiction
A8: ( not v in ww & not w in ww )
proof
hereby ::_thesis: not w in ww
assume v in ww ; ::_thesis: contradiction
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; ::_thesis: verum
end;
assume w in ww ; ::_thesis: contradiction
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; ::_thesis: verum
end;
A9: now__::_thesis:_for_e_being_set_st_e_in_ww_holds_
e_in_vg
let e be set ; ::_thesis: ( e in ww implies e in vg )
assume e in ww ; ::_thesis: e in vg
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 ; ::_thesis: verum
end;
( wwv c= vg & wwv <> vg )
proof
for e being set st e in {v} holds
e in vg by A2, TARSKI:def_1;
then A10: {v} c= vg by TARSKI:def_3;
ww c= vg by A9, TARSKI:def_3;
hence wwv c= vg by A10, XBOOLE_1:8; ::_thesis: wwv <> vg
assume A11: wwv = vg ; ::_thesis: contradiction
not w in {v} by A4, TARSKI:def_1;
hence contradiction by A8, A11, XBOOLE_0:def_3; ::_thesis: verum
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; ::_thesis: verum
end;
hence {v,w} in the SEdges of g ; ::_thesis: verum
end;
thus {v,w} = {v,w} ; ::_thesis: verum
end;
begin
definition
let X be set ;
let g be SimpleGraph of X;
let v1, v2 be Element of g;
let p be FinSequence of the carrier of g;
predp is_path_of v1,v2 means :Def9: :: SGRAPH1:def 9
( 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;
:: deftheorem Def9 defines is_path_of SGRAPH1:def_9_:_
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of g
for p being FinSequence of the carrier of g holds
( p is_path_of v1,v2 iff ( 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))} ) ) ) );
definition
let X be set ;
let g be SimpleGraph of X;
let v1, v2 be Element of the carrier of g;
func PATHS (v1,v2) -> Subset of ( the carrier of g *) equals :: SGRAPH1:def 10
{ ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;
coherence
{ ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } is Subset of ( the carrier of g *)
proof
set IT = { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;
{ ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } c= the carrier of g *
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } or e in the carrier of g * )
assume e in { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ; ::_thesis: e in the carrier of g *
then ex ss being Element of the carrier of g * st
( e = ss & ss is_path_of v1,v2 ) ;
hence e in the carrier of g * ; ::_thesis: verum
end;
hence { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } is Subset of ( the carrier of g *) ; ::_thesis: verum
end;
end;
:: deftheorem defines PATHS SGRAPH1:def_10_:_
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g holds PATHS (v1,v2) = { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;
theorem :: SGRAPH1:32
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g
for 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 :: SGRAPH1:33
for X being set
for g being SimpleGraph of X
for v1, v2 being Element of the carrier of g
for e being Element of the carrier of g * st e is_path_of v1,v2 holds
e in PATHS (v1,v2) ;
definition
let X be set ;
let g be SimpleGraph of X;
let p be set ;
predp is_cycle_of g means :Def11: :: SGRAPH1:def 11
ex v being Element of the carrier of g st p in PATHS (v,v);
end;
:: deftheorem Def11 defines is_cycle_of SGRAPH1:def_11_:_
for X being set
for g being SimpleGraph of X
for p being set holds
( p is_cycle_of g iff ex v being Element of the carrier of g st p in PATHS (v,v) );
begin
definition
let n, m be Element of NAT ;
func K_ (m,n) -> SimpleGraph of NAT means :: SGRAPH1:def 12
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
ex b1 being SimpleGraph of NAT 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)) ) } & b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) )
proof
set VV = Seg (m + n);
set V1 = Seg m;
set V2 = nat_interval ((m + 1),(m + n));
set EE = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } ;
m <= m + n by NAT_1:11;
then A1: Seg m c= Seg (m + n) by FINSEQ_1:5;
A2: nat_interval ((m + 1),(m + n)) c= Seg (m + n) by Th4, NAT_1:11;
{ {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } c= TWOELEMENTSETS (Seg (m + n))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } or e in TWOELEMENTSETS (Seg (m + n)) )
assume e in { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } ; ::_thesis: e in TWOELEMENTSETS (Seg (m + n))
then consider i0, j0 being Element of NAT such that
A3: e = {i0,j0} and
A4: ( i0 in Seg m & j0 in nat_interval ((m + 1),(m + n)) ) ;
( i0 in Seg (m + n) & j0 in Seg (m + n) ) by A1, A2, A4;
then for e0 being set st e0 in e holds
e0 in Seg (m + n) by A3, TARSKI:def_2;
then A5: e c= Seg (m + n) by TARSKI:def_3;
m < m + 1 by NAT_1:13;
then Seg m misses nat_interval ((m + 1),(m + n)) by Th5;
then (Seg m) /\ (nat_interval ((m + 1),(m + n))) = {} by XBOOLE_0:def_7;
then i0 <> j0 by A4, XBOOLE_0:def_4;
hence e in TWOELEMENTSETS (Seg (m + n)) by A1, A2, A3, A4, A5, Th8; ::_thesis: verum
end;
then reconsider EE = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } as finite Subset of (TWOELEMENTSETS (Seg (m + n))) by Th13, FINSET_1:1;
set IT = SimpleGraphStruct(# (Seg (m + n)),EE #);
SimpleGraphStruct(# (Seg (m + n)),EE #) in SIMPLEGRAPHS NAT ;
then reconsider IT = SimpleGraphStruct(# (Seg (m + n)),EE #) as SimpleGraph of NAT by Def4;
reconsider EE = EE as Subset of (TWOELEMENTSETS (Seg (m + n))) ;
take IT ; ::_thesis: 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 #) )
take EE ; ::_thesis: ( 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 #) )
thus ( 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 #) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being SimpleGraph of NAT st 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)) ) } & b1 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) & 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)) ) } & b2 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) holds
b1 = b2 ;
end;
:: deftheorem defines K_ SGRAPH1:def_12_:_
for n, m being Element of NAT
for b3 being SimpleGraph of NAT holds
( b3 = K_ (m,n) iff 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)) ) } & b3 = SimpleGraphStruct(# (Seg (m + n)),ee #) ) );
definition
let n be Element of NAT ;
func K_ n -> SimpleGraph of NAT means :Def13: :: SGRAPH1:def 13
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
ex b1 being SimpleGraph of NAT 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 ) } & b1 = SimpleGraphStruct(# (Seg n),ee #) )
proof
set EE = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } ;
now__::_thesis:_for_e_being_set_st_e_in__{__{i,j}_where_i,_j_is_Element_of_NAT_:_(_i_in_Seg_n_&_j_in_Seg_n_&_i_<>_j_)__}__holds_
e_in_TWOELEMENTSETS_(Seg_n)
let e be set ; ::_thesis: ( e in { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } implies e in TWOELEMENTSETS (Seg n) )
assume e in { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } ; ::_thesis: e in TWOELEMENTSETS (Seg n)
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 ;
e c= Seg n
proof
let e0 be set ; :: according to TARSKI:def_3 ::_thesis: ( not e0 in e or e0 in Seg n )
assume A5: e0 in e ; ::_thesis: e0 in Seg n
percases ( e0 = i0 or e0 = j0 ) by A1, A5, TARSKI:def_2;
suppose e0 = i0 ; ::_thesis: e0 in Seg n
hence e0 in Seg n by A2; ::_thesis: verum
end;
suppose e0 = j0 ; ::_thesis: e0 in Seg n
hence e0 in Seg n by A3; ::_thesis: verum
end;
end;
end;
hence e in TWOELEMENTSETS (Seg n) by A1, A2, A3, A4, Th8; ::_thesis: verum
end;
then { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } c= TWOELEMENTSETS (Seg n) by TARSKI:def_3;
then reconsider EE = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } as finite Subset of (TWOELEMENTSETS (Seg n)) by Th13, FINSET_1:1;
set IT = SimpleGraphStruct(# (Seg n),EE #);
SimpleGraphStruct(# (Seg n),EE #) in SIMPLEGRAPHS NAT ;
then reconsider IT = SimpleGraphStruct(# (Seg n),EE #) as SimpleGraph of NAT by Def4;
take IT ; ::_thesis: 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 #) )
take EE ; ::_thesis: ( 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 #) )
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 #) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being SimpleGraph of NAT st 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 ) } & b1 = SimpleGraphStruct(# (Seg n),ee #) ) & 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 ) } & b2 = SimpleGraphStruct(# (Seg n),ee #) ) holds
b1 = b2 ;
end;
:: deftheorem Def13 defines K_ SGRAPH1:def_13_:_
for n being Element of NAT
for b2 being SimpleGraph of NAT holds
( b2 = K_ n iff 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 ) } & b2 = SimpleGraphStruct(# (Seg n),ee #) ) );
definition
func TriangleGraph -> SimpleGraph of NAT equals :: SGRAPH1:def 14
K_ 3;
correctness
coherence
K_ 3 is SimpleGraph of NAT ;
;
end;
:: deftheorem defines TriangleGraph SGRAPH1:def_14_:_
TriangleGraph = K_ 3;
theorem Th34: :: SGRAPH1:34
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 ; ::_thesis: ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )
now__::_thesis:_for_a_being_set_st_a_in_ee_holds_
a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
let a be set ; ::_thesis: ( a in ee implies b1 in {.{.1,2.},{.2,3.},{.3,1.}.} )
assume a in ee ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
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;
percases ( i = 1 or i = 2 or i = 3 ) by A4, ENUMSET1:def_1, FINSEQ_3:1;
supposeA7: i = 1 ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
now__::_thesis:_a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
percases ( j = 1 or j = 2 or j = 3 ) by A5, ENUMSET1:def_1, FINSEQ_3:1;
suppose j = 1 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A7; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A7, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 3 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A7, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: verum
end;
supposeA8: i = 2 ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
now__::_thesis:_a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
percases ( j = 1 or j = 2 or j = 3 ) by A5, ENUMSET1:def_1, FINSEQ_3:1;
suppose j = 1 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A8, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A8; ::_thesis: verum
end;
suppose j = 3 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A8, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: verum
end;
supposeA9: i = 3 ; ::_thesis: b1 in {.{.1,2.},{.2,3.},{.3,1.}.}
now__::_thesis:_a_in_{.{.1,2.},{.2,3.},{.3,1.}.}
percases ( j = 1 or j = 2 or j = 3 ) by A5, ENUMSET1:def_1, FINSEQ_3:1;
suppose j = 1 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A9, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 2 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A3, A9, ENUMSET1:def_1; ::_thesis: verum
end;
suppose j = 3 ; ::_thesis: a in {.{.1,2.},{.2,3.},{.3,1.}.}
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} by A6, A9; ::_thesis: verum
end;
end;
end;
hence a in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: verum
end;
end;
end;
then A10: ee c= {.{.1,2.},{.2,3.},{.3,1.}.} by TARSKI:def_3;
now__::_thesis:_for_e_being_set_st_e_in_{.{.1,2.},{.2,3.},{.3,1.}.}_holds_
e_in_ee
let e be set ; ::_thesis: ( e in {.{.1,2.},{.2,3.},{.3,1.}.} implies b1 in ee )
assume A11: e in {.{.1,2.},{.2,3.},{.3,1.}.} ; ::_thesis: b1 in ee
percases ( e = {1,2} or e = {2,3} or e = {3,1} ) by A11, ENUMSET1:def_1;
supposeA12: e = {1,2} ; ::_thesis: b1 in ee
now__::_thesis:_ex_i,_j_being_Element_of_NAT_st_
(_e_=_{i,j}_&_i_in_Seg_3_&_j_in_Seg_3_&_i_<>_j_)
take i = 1; ::_thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 2; ::_thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus e = {i,j} by A12; ::_thesis: ( i in Seg 3 & j in Seg 3 & i <> j )
thus ( i in Seg 3 & j in Seg 3 ) by ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: i <> j
thus i <> j ; ::_thesis: verum
end;
hence e in ee by A1; ::_thesis: verum
end;
supposeA13: e = {2,3} ; ::_thesis: b1 in ee
now__::_thesis:_ex_i,_j_being_Element_of_NAT_st_
(_e_=_{i,j}_&_i_in_Seg_3_&_j_in_Seg_3_&_i_<>_j_)
take i = 2; ::_thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 3; ::_thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j ) by A13, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
hence e in ee by A1; ::_thesis: verum
end;
supposeA14: e = {3,1} ; ::_thesis: b1 in ee
now__::_thesis:_ex_i,_j_being_Element_of_NAT_st_
(_e_=_{i,j}_&_i_in_Seg_3_&_j_in_Seg_3_&_i_<>_j_)
take i = 3; ::_thesis: ex j being Element of NAT st
( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
take j = 1; ::_thesis: ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j )
thus ( e = {i,j} & i in Seg 3 & j in Seg 3 & i <> j ) by A14, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
hence e in ee by A1; ::_thesis: verum
end;
end;
end;
then {.{.1,2.},{.2,3.},{.3,1.}.} c= ee by TARSKI:def_3;
hence ( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) ) by A2, A10, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: SGRAPH1:35
( the carrier of TriangleGraph = Seg 3 & the SEdges of TriangleGraph = {.{.1,2.},{.2,3.},{.3,1.}.} ) by Th34;
theorem :: SGRAPH1:36
( {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 :: SGRAPH1:37
((<*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: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 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: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 2 = 2 by FINSEQ_1:66;
reconsider ONE = <*One*>, TWO = <*Two*>, THREE = <*Three*> as FinSequence of the carrier of TriangleGraph ;
((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> = ((ONE ^ TWO) ^ THREE) ^ ONE ;
then reconsider pp = ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> as Element of the carrier of TriangleGraph * by FINSEQ_1:def_11;
A3: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 3 = 3 by FINSEQ_1:66;
A4: (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) . 4 = 1 by FINSEQ_1:66;
A5: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_len_(((<*1*>_^_<*2*>)_^_<*3*>)_^_<*1*>)_holds_
{(pp_._i),(pp_._(i_+_1))}_in_the_SEdges_of_TriangleGraph
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) implies {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph )
assume that
A6: 1 <= i and
A7: i < len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
i < 3 + 1 by A7, FINSEQ_1:66;
then i <= 3 by NAT_1:13;
then A8: i in Seg 3 by A6, FINSEQ_1:1;
percases ( i = 1 or i = 2 or i = 3 ) by A8, ENUMSET1:def_1, FINSEQ_3:1;
suppose i = 1 ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A1, A2, Th34, ENUMSET1:def_1; ::_thesis: verum
end;
suppose i = 2 ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A2, A3, Th34, ENUMSET1:def_1; ::_thesis: verum
end;
suppose i = 3 ; ::_thesis: {(pp . b1),(pp . (b1 + 1))} in the SEdges of TriangleGraph
hence {(pp . i),(pp . (i + 1))} in the SEdges of TriangleGraph by A3, A4, Th34, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
A9: now__::_thesis:_for_i,_j_being_Element_of_NAT_st_1_<=_i_&_i_<_len_pp_&_i_<_j_&_j_<_len_pp_holds_
(_pp_._i_<>_pp_._j_&_{(pp_._i),(pp_._(i_+_1))}_<>_{(pp_._j),(pp_._(j_+_1))}_)
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < len pp & i < j & j < len pp implies ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} ) )
assume that
A10: 1 <= i and
A11: i < len pp and
A12: i < j and
A13: j < len pp ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
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, FINSEQ_1:1;
A16: j < 3 + 1 by A13, FINSEQ_1:66;
then A17: j <= 3 by NAT_1:13;
percases ( i = 1 or i = 2 or i = 3 ) by A15, ENUMSET1:def_1, FINSEQ_3:1;
supposeA18: i = 1 ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 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__::_thesis:_(_pp_._i_<>_pp_._j_&_{(pp_._i),(pp_._(i_+_1))}_<>_{(pp_._j),(pp_._(j_+_1))}_)
percases ( j = 2 or j = 3 ) by A20, XXREAL_0:1;
supposeA21: j = 2 ; ::_thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
hence pp . i <> pp . j by A19, FINSEQ_1:66; ::_thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A2, A3, A18, A21, ZFMISC_1:6; ::_thesis: verum
end;
supposeA22: j = 3 ; ::_thesis: ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} )
hence pp . i <> pp . j by A19, FINSEQ_1:66; ::_thesis: {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))}
thus {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} by A1, A2, A3, A18, A22, ZFMISC_1:6; ::_thesis: verum
end;
end;
end;
hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) ; ::_thesis: verum
end;
supposeA23: i = 2 ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
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; ::_thesis: verum
end;
suppose i = 3 ; ::_thesis: ( pp . b1 <> pp . b2 & {(pp . b1),(pp . (b1 + 1))} <> {(pp . b2),(pp . (b2 + 1))} )
hence ( pp . i <> pp . j & {(pp . i),(pp . (i + 1))} <> {(pp . j),(pp . (j + 1))} ) by A12, A16, NAT_1:13; ::_thesis: verum
end;
end;
end;
len (((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*>) = 4 by FINSEQ_1:66;
then pp is_path_of o,o by A1, A4, A5, A9, Def9;
then pp in PATHS (o,o) ;
hence ((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph by Def11; ::_thesis: verum
end;