environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions 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;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XXREAL_0, NAT_1, FINSEQ_1, CARD_1, XTUPLE_0, XCMPLX_0;
constructors HIDDEN, WELLORD2, SETWISEO, NAT_1, FINSEQ_2, STRUCT_0, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1;
expansions TARSKI;
Lm1:
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
scheme
IndSimpleGraphs0{
F1()
-> set ,
P1[
set ] } :
provided
definition
let n,
m be
Element of
NAT ;
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;
definition
let n be
Element of
NAT ;
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;
:: 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 (-: