begin
begin
theorem
theorem Nat0:
for
x,
y,
z being
Nat holds
(
x in y \ z iff (
z <= x &
x < y ) )
theorem U5s:
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 U5:
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 Sym0a:
theorem Sym0:
begin
theorem Partcard:
:: 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 Tpart0:
theorem Tpart1:
theorem Tsr0:
begin
:: deftheorem Lwfchr 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 Lchro 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 Lwfcc 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 Lclico 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 Maxclique:
theorem
theorem Maxchromatic:
theorem
theorem CliChr:
theorem
begin
theorem DCompl:
theorem DCompl1:
theorem CliStaCompl:
theorem CliComplSta:
theorem StaCliCompl:
theorem StaComplCli:
theorem cliRstaCR:
theorem
theorem ChrClicoCompl:
theorem ClicoComplChr:
theorem ClicoChrCompl:
theorem ChrComplClico:
theorem chrRcovCR:
theorem
begin
:: deftheorem LAdjset 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 AdjCol:
begin
:: deftheorem LNRS 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 LCRS 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 CRS:
theorem CompleteCli:
theorem
theorem CompleteChr:
theorem
begin
definition
let n be
Nat;
let R be
NatRelStr of
n;
func Mycielskian R -> NatRelStr of
(2 * n) + 1
means :
LMR:
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 LMR 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 cMR0:
theorem iMR0:
theorem iMR1ba:
theorem iMR1b:
theorem iMR1a:
theorem iMR1c:
theorem iMR1d:
theorem iMR1e:
theorem Msubrel:
theorem MClique:
theorem Tchro0:
theorem Mchromatic:
:: deftheorem LMycn 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 Mycn1:
theorem Mycth:
theorem
theorem