begin
begin
theorem
theorem Th2:
for
x,
y,
z being
Nat holds
(
x in y \ z iff (
z <= x &
x < y ) )
theorem Th3:
for
A,
B,
C,
D,
E,
X being
set st (
X c= A or
X c= B or
X c= C or
X c= D or
X c= E ) holds
X c= (((A \/ B) \/ C) \/ D) \/ E
theorem Th4:
for
A,
B,
C,
D,
E,
x being
set holds
(
x in (((A \/ B) \/ C) \/ D) \/ E iff (
x in A or
x in B or
x in C or
x in D or
x in E ) )
theorem Th5:
theorem Th6:
begin
theorem Th7:
:: deftheorem defines | MYCIELSK:def 1 :
for X being set
for P being a_partition of X
for S being Subset of X holds P | S = { (x /\ S) where x is Element of P : x meets S } ;
theorem Th8:
theorem Th9:
theorem Th10:
begin
:: deftheorem Def2 defines with_finite_chromatic# MYCIELSK:def 2 :
for R being RelStr holds
( R is with_finite_chromatic# iff ex C being Coloring of R st C is finite );
:: deftheorem Def3 defines chromatic# MYCIELSK:def 3 :
for R being with_finite_chromatic# RelStr
for b2 being Nat holds
( b2 = chromatic# R iff ( ex C being finite Coloring of R st card C = b2 & ( for C being finite Coloring of R holds b2 <= card C ) ) );
:: deftheorem Def4 defines with_finite_cliquecover# MYCIELSK:def 4 :
for R being RelStr holds
( R is with_finite_cliquecover# iff ex C being Clique-partition of R st C is finite );
:: deftheorem Def5 defines cliquecover# MYCIELSK:def 5 :
for R being with_finite_cliquecover# RelStr
for b2 being Nat holds
( b2 = cliquecover# R iff ( ex C being finite Clique-partition of R st card C = b2 & ( for C being finite Clique-partition of R holds b2 <= card C ) ) );
theorem Th11:
theorem
theorem Th13:
theorem
theorem Th15:
theorem
begin
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
begin
:: deftheorem Def6 defines Adjacent MYCIELSK:def 6 :
for R being RelStr
for v being Element of R
for b3 being Subset of R holds
( b3 = Adjacent v iff for x being Element of R holds
( x in b3 iff ( x < v or v < x ) ) );
theorem Th31:
begin
:: deftheorem Def7 defines NatRelStr MYCIELSK:def 7 :
for n being Nat
for b2 being strict RelStr holds
( b2 is NatRelStr of n iff the carrier of b2 = n );
:: deftheorem Def8 defines CompleteRelStr MYCIELSK:def 8 :
for n being Nat
for b2 being NatRelStr of n holds
( b2 = CompleteRelStr n iff the InternalRel of b2 = [:n,n:] \ (id n) );
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
begin
definition
let n be
Nat;
let R be
NatRelStr of
n;
func Mycielskian R -> NatRelStr of
(2 * n) + 1
means :
Def9:
the
InternalRel of
it = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:];
existence
ex b1 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:]
uniqueness
for b1, b2 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] & the InternalRel of b2 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] holds
b1 = b2
end;
:: deftheorem Def9 defines Mycielskian MYCIELSK:def 9 :
for n being Nat
for R being NatRelStr of n
for b3 being NatRelStr of (2 * n) + 1 holds
( b3 = Mycielskian R iff the InternalRel of b3 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] );
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
:: deftheorem Def10 defines Mycielskian MYCIELSK:def 10 :
for n being Nat
for b2 being NatRelStr of (3 * (2 |^ n)) -' 1 holds
( b2 = Mycielskian n iff ex myc being Function st
( b2 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) ) );
theorem Th49:
theorem Th50:
theorem
theorem