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 )
:: deftheorem defines nat_interval SGRAPH1:def 1 :
theorem
canceled;
theorem
theorem
theorem
theorem Th5:
theorem Th6:
theorem
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
:: deftheorem SGRAPH1:def 2 :
canceled;
:: deftheorem SGRAPH1:def 3 :
canceled;
:: deftheorem defines TWOELEMENTSETS SGRAPH1:def 4 :
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
theorem
begin
:: deftheorem SGRAPH1:def 5 :
canceled;
:: deftheorem defines SIMPLEGRAPHS SGRAPH1:def 6 :
theorem
canceled;
theorem Th19:
:: deftheorem Def7 defines SimpleGraph SGRAPH1:def 7 :
theorem
canceled;
theorem Th21:
begin
theorem
canceled;
theorem Th23:
theorem
canceled;
theorem
theorem
theorem Th27:
:: deftheorem defines is_isomorphic_to SGRAPH1:def 8 :
begin
scheme
IndSimpleGraphs0{
F1()
-> set ,
P1[
set ] } :
provided
theorem
theorem
canceled;
theorem Th30:
theorem Th31:
:: deftheorem Def9 defines is_SetOfSimpleGraphs_of SGRAPH1:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th35:
theorem Th36:
theorem
begin
:: deftheorem defines SubGraph SGRAPH1:def 10 :
begin
:: deftheorem Def11 defines degree SGRAPH1:def 11 :
theorem
canceled;
theorem Th39:
theorem
theorem
theorem
begin
:: deftheorem Def12 defines is_path_of SGRAPH1:def 12 :
:: deftheorem defines PATHS SGRAPH1:def 13 :
theorem
canceled;
theorem
theorem
:: deftheorem Def14 defines is_cycle_of SGRAPH1:def 14 :
begin
definition
let n,
m be
Element of
NAT ;
canceled;func K_ m,
n -> SimpleGraph of
NAT means
ex
ee being
Subset of
(TWOELEMENTSETS (Seg (m + n))) st
(
ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval (m + 1),(m + n) ) } &
it = SimpleGraphStruct(#
(Seg (m + n)),
ee #) );
existence
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 #) )
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 SGRAPH1:def 15 :
canceled;
:: deftheorem defines K_ SGRAPH1:def 16 :
definition
let n be
Element of
NAT ;
func K_ n -> SimpleGraph of
NAT means :
Def17:
ex
ee being
finite Subset of
(TWOELEMENTSETS (Seg n)) st
(
ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } &
it = SimpleGraphStruct(#
(Seg n),
ee #) );
existence
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 #) )
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 Def17 defines K_ SGRAPH1:def 17 :
:: deftheorem defines TriangleGraph SGRAPH1:def 18 :
theorem Th46:
theorem
theorem
theorem