:: MYCIELSK semantic presentation
begin
begin
theorem :: MYCIELSK:1
for x, y, z being real number st 0 <= x holds
x * (y -' z) = (x * y) -' (x * z)
proof
let x, y, z be real number ; ::_thesis: ( 0 <= x implies x * (y -' z) = (x * y) -' (x * z) )
assume A1: x >= 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z)
percases ( y - z >= 0 or y - z < 0 ) ;
supposeA2: y - z >= 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z)
A3: x * (y - z) >= 0 by A1, A2;
thus x * (y -' z) = x * (y - z) by A2, XREAL_0:def_2
.= (x * y) - (x * z)
.= (x * y) -' (x * z) by A3, XREAL_0:def_2 ; ::_thesis: verum
end;
supposeA4: y - z < 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z)
percases ( x = 0 or x > 0 ) by A1;
supposeA5: x = 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z)
thus x * (y -' z) = (x * y) -' (x * z) by A5, XREAL_1:232; ::_thesis: verum
end;
supposeA6: x > 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z)
x * (y - z) < 0 by A4, A6;
then A7: (x * y) - (x * z) < 0 ;
thus x * (y -' z) = x * 0 by A4, XREAL_0:def_2
.= (x * y) -' (x * z) by A7, XREAL_0:def_2 ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th2: :: MYCIELSK:2
for x, y, z being Nat holds
( x in y \ z iff ( z <= x & x < y ) )
proof
let x, y, z be Nat; ::_thesis: ( x in y \ z iff ( z <= x & x < y ) )
hereby ::_thesis: ( z <= x & x < y implies x in y \ z )
assume A1: x in y \ z ; ::_thesis: ( z <= x & x < y )
not x in z by A1, XBOOLE_0:def_5;
hence z <= x by NAT_1:44; ::_thesis: x < y
thus x < y by A1, NAT_1:44; ::_thesis: verum
end;
assume ( z <= x & x < y ) ; ::_thesis: x in y \ z
then ( x in y & not x in z ) by NAT_1:44;
hence x in y \ z by XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th3: :: MYCIELSK:3
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
proof
let A, B, C, D, E, X be set ; ::_thesis: ( ( X c= A or X c= B or X c= C or X c= D or X c= E ) implies X c= (((A \/ B) \/ C) \/ D) \/ E )
assume A1: ( X c= A or X c= B or X c= C or X c= D or X c= E ) ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
percases ( X c= A or X c= B or X c= C or X c= D or X c= E ) by A1;
suppose X c= A ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= A \/ B by XBOOLE_1:10;
then X c= (A \/ B) \/ C by XBOOLE_1:10;
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum
end;
suppose X c= B ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= A \/ B by XBOOLE_1:10;
then X c= (A \/ B) \/ C by XBOOLE_1:10;
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum
end;
suppose X c= C ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= (A \/ B) \/ C by XBOOLE_1:10;
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum
end;
suppose X c= D ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10;
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum
end;
suppose X c= E ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E
hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum
end;
end;
end;
theorem Th4: :: MYCIELSK:4
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 ) )
proof
let A, B, C, D, E, x be set ; ::_thesis: ( 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 ) )
hereby ::_thesis: ( ( x in A or x in B or x in C or x in D or x in E ) implies x in (((A \/ B) \/ C) \/ D) \/ E )
assume x in (((A \/ B) \/ C) \/ D) \/ E ; ::_thesis: ( x in A or x in B or x in C or x in D or x in E )
then ( x in ((A \/ B) \/ C) \/ D or x in E ) by XBOOLE_0:def_3;
then ( x in (A \/ B) \/ C or x in D or x in E ) by XBOOLE_0:def_3;
then ( x in A \/ B or x in C or x in D or x in E ) by XBOOLE_0:def_3;
hence ( x in A or x in B or x in C or x in D or x in E ) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A1: ( x in A or x in B or x in C or x in D or x in E ) ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E
percases ( x in A or x in B or x in C or x in D or x in E ) by A1;
suppose x in A ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E
then x in A \/ B by XBOOLE_0:def_3;
then x in (A \/ B) \/ C by XBOOLE_0:def_3;
then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in B ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E
then x in A \/ B by XBOOLE_0:def_3;
then x in (A \/ B) \/ C by XBOOLE_0:def_3;
then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in C ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E
then x in (A \/ B) \/ C by XBOOLE_0:def_3;
then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in D ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E
then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3;
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x in E ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E
hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
theorem Th5: :: MYCIELSK:5
for R being symmetric RelStr
for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds
[y,x] in the InternalRel of R
proof
let R be symmetric RelStr ; ::_thesis: for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds
[y,x] in the InternalRel of R
let x, y be set ; ::_thesis: ( x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R implies [y,x] in the InternalRel of R )
set cR = the carrier of R;
set iR = the InternalRel of R;
assume that
A1: x in the carrier of R and
A2: y in the carrier of R and
A3: [x,y] in the InternalRel of R ; ::_thesis: [y,x] in the InternalRel of R
the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def_3;
hence [y,x] in the InternalRel of R by A1, A2, A3, RELAT_2:def_3; ::_thesis: verum
end;
theorem Th6: :: MYCIELSK:6
for R being symmetric RelStr
for x, y being Element of R st x <= y holds
y <= x
proof
let R be symmetric RelStr ; ::_thesis: for x, y being Element of R st x <= y holds
y <= x
let x, y be Element of R; ::_thesis: ( x <= y implies y <= x )
assume A1: x <= y ; ::_thesis: y <= x
set cR = the carrier of R;
set iR = the InternalRel of R;
A2: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def_3;
A3: [x,y] in the InternalRel of R by A1, ORDERS_2:def_5;
then ( x in the carrier of R & y in the carrier of R ) by ZFMISC_1:87;
then [y,x] in the InternalRel of R by A2, A3, RELAT_2:def_3;
hence y <= x by ORDERS_2:def_5; ::_thesis: verum
end;
begin
theorem Th7: :: MYCIELSK:7
for X being set
for P being a_partition of X holds card P c= card X
proof
let X be set ; ::_thesis: for P being a_partition of X holds card P c= card X
let P be a_partition of X; ::_thesis: card P c= card X
defpred S1[ set , set ] means $2 = choose $1;
A1: for e being set st e in P holds
ex u being set st S1[e,u] ;
consider f being Function such that
A2: dom f = P and
A3: for e being set st e in P holds
S1[e,f . e] from CLASSES1:sch_1(A1);
A4: f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f . x1 = f . x2 ; ::_thesis: x1 = x2
A8: x1 <> {} by A2, A5, EQREL_1:def_4;
A9: x2 <> {} by A2, A6, EQREL_1:def_4;
( f . x1 = choose x1 & f . x2 = choose x2 ) by A5, A6, A2, A3;
then x1 meets x2 by A7, A8, A9, XBOOLE_0:3;
hence x1 = x2 by A5, A6, A2, EQREL_1:def_4; ::_thesis: verum
end;
rng f c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in X )
assume y in rng f ; ::_thesis: y in X
then consider x being set such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def_3;
A12: f . x = choose x by A2, A3, A10;
x <> {} by A2, A10, EQREL_1:def_4;
then f . x in x by A12;
hence y in X by A10, A2, A11; ::_thesis: verum
end;
hence card P c= card X by A2, A4, CARD_1:10; ::_thesis: verum
end;
definition
let X be set ;
let P be a_partition of X;
let S be Subset of X;
funcP | S -> a_partition of S equals :: MYCIELSK:def 1
{ (x /\ S) where x is Element of P : x meets S } ;
coherence
{ (x /\ S) where x is Element of P : x meets S } is a_partition of S
proof
set D = { (x /\ S) where x is Element of P : x meets S } ;
A1: { (x /\ S) where x is Element of P : x meets S } c= bool S
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x /\ S) where x is Element of P : x meets S } or a in bool S )
assume a in { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: a in bool S
then consider x being Element of P such that
A2: a = x /\ S and
x meets S ;
a c= S by A2, XBOOLE_1:17;
hence a in bool S ; ::_thesis: verum
end;
A3: union { (x /\ S) where x is Element of P : x meets S } = S
proof
thus union { (x /\ S) where x is Element of P : x meets S } c= S :: according to XBOOLE_0:def_10 ::_thesis: S c= union { (x /\ S) where x is Element of P : x meets S }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (x /\ S) where x is Element of P : x meets S } or x in S )
assume x in union { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: x in S
then consider Y being set such that
A4: x in Y and
A5: Y in { (x /\ S) where x is Element of P : x meets S } by TARSKI:def_4;
thus x in S by A4, A1, A5; ::_thesis: verum
end;
thus S c= union { (x /\ S) where x is Element of P : x meets S } ::_thesis: verum
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in S or s in union { (x /\ S) where x is Element of P : x meets S } )
assume A6: s in S ; ::_thesis: s in union { (x /\ S) where x is Element of P : x meets S }
then s in X ;
then s in union P by EQREL_1:def_4;
then consider p being set such that
A7: s in p and
A8: p in P by TARSKI:def_4;
p meets S by A7, A6, XBOOLE_0:3;
then A9: p /\ S in { (x /\ S) where x is Element of P : x meets S } by A8;
s in p /\ S by A7, A6, XBOOLE_0:def_4;
hence s in union { (x /\ S) where x is Element of P : x meets S } by A9, TARSKI:def_4; ::_thesis: verum
end;
end;
now__::_thesis:_for_A_being_Subset_of_S_st_A_in__{__(x_/\_S)_where_x_is_Element_of_P_:_x_meets_S__}__holds_
(_A_<>_{}_&_(_for_B_being_Subset_of_S_holds_
(_not_B_in__{__(x_/\_S)_where_x_is_Element_of_P_:_x_meets_S__}__or_A_=_B_or_A_misses_B_)_)_)
let A be Subset of S; ::_thesis: ( A in { (x /\ S) where x is Element of P : x meets S } implies ( A <> {} & ( for B being Subset of S holds
( not B in { (x /\ S) where x is Element of P : x meets S } or b2 = b3 or b2 misses b3 ) ) ) )
assume A in { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: ( A <> {} & ( for B being Subset of S holds
( not B in { (x /\ S) where x is Element of P : x meets S } or b2 = b3 or b2 misses b3 ) ) )
then consider x being Element of P such that
A10: A = x /\ S and
A11: x meets S ;
consider z being set such that
A12: z in x and
A13: z in S by A11, XBOOLE_0:3;
reconsider Xp1 = X as non empty set by A13;
reconsider Pp1 = P as a_partition of Xp1 ;
thus A <> {} by A12, A13, A10, XBOOLE_0:def_4; ::_thesis: for B being Subset of S holds
( not B in { (x /\ S) where x is Element of P : x meets S } or b2 = b3 or b2 misses b3 )
let B be Subset of S; ::_thesis: ( not B in { (x /\ S) where x is Element of P : x meets S } or b1 = b2 or b1 misses b2 )
assume B in { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: ( b1 = b2 or b1 misses b2 )
then consider y being Element of P such that
A14: B = y /\ S and
y meets S ;
A15: ( x in Pp1 & y in Pp1 ) ;
percases ( x = y or x misses y ) by A15, EQREL_1:def_4;
suppose x = y ; ::_thesis: ( b1 = b2 or b1 misses b2 )
hence ( A = B or A misses B ) by A10, A14; ::_thesis: verum
end;
suppose x misses y ; ::_thesis: ( b1 = b2 or b1 misses b2 )
hence ( A = B or A misses B ) by A10, A14, XBOOLE_1:76; ::_thesis: verum
end;
end;
end;
hence { (x /\ S) where x is Element of P : x meets S } is a_partition of S by A1, A3, EQREL_1:def_4; ::_thesis: verum
end;
end;
:: 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 } ;
registration
let X be set ;
cluster finite V89() for a_partition of X;
existence
ex b1 being a_partition of X st b1 is finite
proof
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: ex b1 being a_partition of X st b1 is finite
hence ex b1 being a_partition of X st b1 is finite by EQREL_1:45; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: ex b1 being a_partition of X st b1 is finite
then {X} is a_partition of X by EQREL_1:39;
hence ex b1 being a_partition of X st b1 is finite ; ::_thesis: verum
end;
end;
end;
end;
registration
let X be set ;
let P be finite a_partition of X;
let S be Subset of X;
clusterP | S -> finite ;
coherence
P | S is finite
proof
defpred S1[ set , set ] means P = X /\ S;
A1: for e being set st e in P holds
ex u being set st S1[e,u] ;
consider f being Function such that
A2: dom f = P and
A3: for e being set st e in P holds
S1[e,f . e] from CLASSES1:sch_1(A1);
A4: rng f is finite by A2, FINSET_1:8;
P | S c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P | S or x in rng f )
assume x in P | S ; ::_thesis: x in rng f
then consider xx being Element of P such that
A5: x = xx /\ S and
A6: xx meets S ;
consider y being set such that
y in xx and
A7: y in S by A6, XBOOLE_0:3;
reconsider Xp1 = X as non empty set by A7;
A8: P is a_partition of Xp1 ;
then x = f . xx by A3, A5;
hence x in rng f by A8, A2, FUNCT_1:def_3; ::_thesis: verum
end;
hence P | S is finite by A4; ::_thesis: verum
end;
end;
theorem Th8: :: MYCIELSK:8
for X being set
for P being finite a_partition of X
for S being Subset of X holds card (P | S) <= card P
proof
let X be set ; ::_thesis: for P being finite a_partition of X
for S being Subset of X holds card (P | S) <= card P
let P be finite a_partition of X; ::_thesis: for S being Subset of X holds card (P | S) <= card P
let S be Subset of X; ::_thesis: card (P | S) <= card P
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: card (P | S) <= card P
then A2: P = {} by EQREL_1:32;
S = {} by A1;
hence card (P | S) <= card P by A2, EQREL_1:32; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: card (P | S) <= card P
then reconsider Pp1 = P as non empty finite set ;
defpred S1[ set ] means $1 meets S;
deffunc H1( set ) -> Element of bool X = $1 /\ S;
A3: P | S = { H1(x) where x is Element of Pp1 : S1[x] } ;
card (P | S) <= card Pp1 from DILWORTH:sch_1(A3);
hence card (P | S) <= card P ; ::_thesis: verum
end;
end;
end;
theorem Th9: :: MYCIELSK:9
for X being set
for P being finite a_partition of X
for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
proof
let X be set ; ::_thesis: for P being finite a_partition of X
for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
let P be finite a_partition of X; ::_thesis: for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
let S be Subset of X; ::_thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
hereby ::_thesis: ( card (P | S) = card P implies for p being set st p in P holds
p meets S )
assume for p being set st p in P holds
p meets S ; ::_thesis: card (P | S) = card P
S = {} by A1;
hence card (P | S) = {} by CARD_1:27, EQREL_1:32
.= card P by A1, CARD_1:27, EQREL_1:32 ;
::_thesis: verum
end;
thus ( card (P | S) = card P implies for p being set st p in P holds
p meets S ) by A1, EQREL_1:32; ::_thesis: verum
end;
supposeA2: X <> {} ; ::_thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
set PS = P | S;
reconsider Pp1 = P as non empty finite set by A2;
hereby ::_thesis: ( card (P | S) = card P implies for p being set st p in P holds
p meets S )
assume A3: for p being set st p in P holds
p meets S ; ::_thesis: card (P | S) = card P
set p = the Element of P;
the Element of P in Pp1 ;
then the Element of P meets S by A3;
then the Element of P /\ S in P | S ;
then reconsider PSp1 = P | S as non empty finite set ;
defpred S1[ set , set ] means ( $1 in P & $2 = $1 /\ S );
A4: for x being set st x in P holds
ex y being set st
( y in PSp1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in P implies ex y being set st
( y in PSp1 & S1[x,y] ) )
assume A5: x in P ; ::_thesis: ex y being set st
( y in PSp1 & S1[x,y] )
take x /\ S ; ::_thesis: ( x /\ S in PSp1 & S1[x,x /\ S] )
x meets S by A5, A3;
hence ( x /\ S in PSp1 & S1[x,x /\ S] ) by A5; ::_thesis: verum
end;
consider f being Function of P,PSp1 such that
A6: for x being set st x in P holds
S1[x,f . x] from FUNCT_2:sch_1(A4);
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_P_&_x2_in_P_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in P & x2 in P & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in P and
A8: x2 in P and
A9: f . x1 = f . x2 ; ::_thesis: x1 = x2
A10: f . x1 = x1 /\ S by A7, A6;
A11: f . x2 = x2 /\ S by A8, A6;
x1 meets S by A7, A3;
then f . x1 in P | S by A10, A7;
then f . x1 <> {} by EQREL_1:def_4;
then consider x being set such that
A12: x in f . x1 by XBOOLE_0:def_1;
( x in x1 & x in x2 ) by A12, A9, A10, A11, XBOOLE_0:def_4;
then x1 meets x2 by XBOOLE_0:3;
hence x1 = x2 by A7, A8, EQREL_1:def_4; ::_thesis: verum
end;
then A13: f is one-to-one by FUNCT_2:19;
rng f = PSp1
proof
thus rng f c= PSp1 :: according to XBOOLE_0:def_10 ::_thesis: PSp1 c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in PSp1 )
assume y in rng f ; ::_thesis: y in PSp1
then consider x being set such that
A14: x in P and
A15: f . x = y by FUNCT_2:11;
x meets S by A3, A14;
then x /\ S in P | S by A14;
hence y in PSp1 by A15, A14, A6; ::_thesis: verum
end;
thus PSp1 c= rng f ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in PSp1 or y in rng f )
assume y in PSp1 ; ::_thesis: y in rng f
then consider p being Element of P such that
A16: y = p /\ S and
p meets S ;
A17: p in Pp1 ;
then f . p = p /\ S by A6;
hence y in rng f by A16, A17, FUNCT_2:4; ::_thesis: verum
end;
end;
then f is onto by FUNCT_2:def_3;
hence card (P | S) = card P by A13, EULER_1:11; ::_thesis: verum
end;
assume A18: card (P | S) = card P ; ::_thesis: for p being set st p in P holds
p meets S
defpred S1[ set , set ] means ( $1 in P | S & $2 in Pp1 & $1 = $2 /\ S );
A19: for x being set st x in P | S holds
ex y being set st
( y in Pp1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in P | S implies ex y being set st
( y in Pp1 & S1[x,y] ) )
assume A20: x in P | S ; ::_thesis: ex y being set st
( y in Pp1 & S1[x,y] )
then consider p being Element of P such that
A21: x = p /\ S and
p meets S ;
take p ; ::_thesis: ( p in Pp1 & S1[x,p] )
thus ( p in Pp1 & S1[x,p] ) by A20, A21; ::_thesis: verum
end;
consider f being Function of (P | S),Pp1 such that
A22: for x being set st x in P | S holds
S1[x,f . x] from FUNCT_2:sch_1(A19);
A23: f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A24: x1 in dom f and
A25: x2 in dom f and
A26: f . x1 = f . x2 ; ::_thesis: x1 = x2
x1 = (f . x1) /\ S by A24, A22;
hence x1 = x2 by A26, A25, A22; ::_thesis: verum
end;
A27: rng f = P by A18, A23, FINSEQ_4:63;
let p be set ; ::_thesis: ( p in P implies p meets S )
assume p in P ; ::_thesis: p meets S
then consider ps being set such that
A28: ps in dom f and
A29: p = f . ps by A27, FUNCT_1:def_3;
A30: dom f = P | S by FUNCT_2:def_1;
A31: ps = p /\ S by A29, A28, A22;
not ps is empty by A28, A30, EQREL_1:def_4;
then ex x being set st x in ps by XBOOLE_0:def_1;
hence p meets S by A31, XBOOLE_0:4; ::_thesis: verum
end;
end;
end;
theorem Th10: :: MYCIELSK:10
for R being RelStr
for C being Coloring of R
for S being Subset of R holds C | S is Coloring of (subrelstr S)
proof
let R be RelStr ; ::_thesis: for C being Coloring of R
for S being Subset of R holds C | S is Coloring of (subrelstr S)
let C be Coloring of R; ::_thesis: for S being Subset of R holds C | S is Coloring of (subrelstr S)
let S be Subset of R; ::_thesis: C | S is Coloring of (subrelstr S)
set sS = subrelstr S;
A1: the carrier of (subrelstr S) = S by YELLOW_0:def_15;
now__::_thesis:_for_x_being_set_st_x_in_C_|_S_holds_
x_is_StableSet_of_(subrelstr_S)
let x be set ; ::_thesis: ( x in C | S implies x is StableSet of (subrelstr S) )
assume x in C | S ; ::_thesis: x is StableSet of (subrelstr S)
then consider c being Element of C such that
A2: x = c /\ S and
A3: c meets S ;
consider z being set such that
z in c and
A4: z in S by A3, XBOOLE_0:3;
A5: not subrelstr S is empty by A4, YELLOW_0:def_15;
A6: not R is empty by A4;
reconsider Rp1 = R as non empty RelStr by A4;
reconsider xp1 = x as Subset of (subrelstr S) by A1, A2, XBOOLE_1:17;
xp1 is stable
proof
let a, b be Element of (subrelstr S); :: according to DILWORTH:def_2 ::_thesis: ( not a in xp1 or not b in xp1 or a = b or ( not a <= b & not b <= a ) )
assume that
A7: a in xp1 and
A8: b in xp1 and
A9: a <> b ; ::_thesis: ( not a <= b & not b <= a )
A10: ( a in c & b in c ) by A7, A8, A2, XBOOLE_0:def_4;
reconsider ap1 = a, bp1 = b as Element of R by A5, A6, YELLOW_0:58;
A11: C is Coloring of Rp1 ;
then c in C ;
then reconsider cp1 = c as Subset of R ;
A12: cp1 is stable by A11, DILWORTH:def_12;
assume ( a <= b or b <= a ) ; ::_thesis: contradiction
then ( ap1 <= bp1 or bp1 <= ap1 ) by YELLOW_0:59;
hence contradiction by A9, A10, A12, DILWORTH:def_2; ::_thesis: verum
end;
hence x is StableSet of (subrelstr S) ; ::_thesis: verum
end;
hence C | S is Coloring of (subrelstr S) by A1, DILWORTH:def_12; ::_thesis: verum
end;
begin
definition
let R be RelStr ;
attrR is with_finite_chromatic# means :Def2: :: MYCIELSK:def 2
ex C being Coloring of R st C is finite ;
end;
:: 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 );
registration
cluster with_finite_chromatic# for RelStr ;
existence
ex b1 being RelStr st b1 is with_finite_chromatic#
proof
take R = the empty RelStr ; ::_thesis: R is with_finite_chromatic#
reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
take S ; :: according to MYCIELSK:def_2 ::_thesis: S is finite
thus S is finite ; ::_thesis: verum
end;
end;
registration
cluster finite -> with_finite_chromatic# for RelStr ;
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_chromatic#
proof
let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_chromatic# )
set cR = the carrier of R;
assume A1: R is finite ; ::_thesis: R is with_finite_chromatic#
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: R is with_finite_chromatic#
then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
for x being set st x in S holds
x is StableSet of R ;
then reconsider S = S as Coloring of R by DILWORTH:def_12;
take S ; :: according to MYCIELSK:def_2 ::_thesis: S is finite
thus S is finite ; ::_thesis: verum
end;
supposeA2: not R is empty ; ::_thesis: R is with_finite_chromatic#
reconsider cRp1 = the carrier of R as non empty finite set by A2, A1;
set S = SmallestPartition the carrier of R;
deffunc H1( set ) -> set = {c1};
defpred S1[ set ] means verum;
A3: SmallestPartition the carrier of R = { H1(x) where x is Element of cRp1 : S1[x] } by EQREL_1:37;
A4: { H1(x) where x is Element of cRp1 : S1[x] } is finite from PRE_CIRC:sch_1();
now__::_thesis:_for_z_being_set_st_z_in_SmallestPartition_the_carrier_of_R_holds_
z_is_StableSet_of_R
let z be set ; ::_thesis: ( z in SmallestPartition the carrier of R implies z is StableSet of R )
assume z in SmallestPartition the carrier of R ; ::_thesis: z is StableSet of R
then ex x being Element of the carrier of R st z = {x} by A3;
hence z is StableSet of R by A2, SUBSET_1:33; ::_thesis: verum
end;
then reconsider S = SmallestPartition the carrier of R as Coloring of R by DILWORTH:def_12;
take S ; :: according to MYCIELSK:def_2 ::_thesis: S is finite
thus S is finite by A4; ::_thesis: verum
end;
end;
end;
end;
registration
let R be with_finite_chromatic# RelStr ;
cluster finite V89() StableSet-wise for a_partition of the carrier of R;
existence
ex b1 being Coloring of R st b1 is finite by Def2;
end;
registration
let R be with_finite_chromatic# RelStr ;
let S be Subset of R;
cluster subrelstr S -> with_finite_chromatic# ;
coherence
subrelstr S is with_finite_chromatic#
proof
set sS = subrelstr S;
consider C being Coloring of R such that
A1: C is finite by Def2;
A2: the carrier of (subrelstr S) = S by YELLOW_0:def_15;
reconsider CS = C | S as a_partition of S ;
for x being set st x in CS holds
x is StableSet of (subrelstr S)
proof
let x be set ; ::_thesis: ( x in CS implies x is StableSet of (subrelstr S) )
assume x in CS ; ::_thesis: x is StableSet of (subrelstr S)
then consider X being Element of C such that
A3: x = X /\ S and
A4: X meets S ;
ex y being set st
( y in X & y in S ) by A4, XBOOLE_0:3;
then X is StableSet of R by DILWORTH:def_12;
hence x is StableSet of (subrelstr S) by A3, DILWORTH:31; ::_thesis: verum
end;
then CS is Coloring of (subrelstr S) by A2, DILWORTH:def_12;
hence subrelstr S is with_finite_chromatic# by A1, Def2; ::_thesis: verum
end;
end;
definition
let R be with_finite_chromatic# RelStr ;
func chromatic# R -> Nat means :Def3: :: MYCIELSK:def 3
( ex C being finite Coloring of R st card C = it & ( for C being finite Coloring of R holds it <= card C ) );
existence
ex b1 being Nat st
( ex C being finite Coloring of R st card C = b1 & ( for C being finite Coloring of R holds b1 <= card C ) )
proof
defpred S1[ Nat] means ex C being finite Coloring of R st card C = $1;
consider C being Coloring of R such that
A1: C is finite by Def2;
card C = card C ;
then A2: ex k being Nat st S1[k] by A1;
consider n being Nat such that
A3: S1[n] and
A4: for k being Nat st S1[k] holds
n <= k from NAT_1:sch_5(A2);
take n ; ::_thesis: ( ex C being finite Coloring of R st card C = n & ( for C being finite Coloring of R holds n <= card C ) )
thus ex C being finite Coloring of R st card C = n by A3; ::_thesis: for C being finite Coloring of R holds n <= card C
let C be finite Coloring of R; ::_thesis: n <= card C
thus n <= card C by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Nat st ex C being finite Coloring of R st card C = b1 & ( for C being finite Coloring of R holds b1 <= card C ) & ex C being finite Coloring of R st card C = b2 & ( for C being finite Coloring of R holds b2 <= card C ) holds
b1 = b2
proof
let it1, it2 be Nat; ::_thesis: ( ex C being finite Coloring of R st card C = it1 & ( for C being finite Coloring of R holds it1 <= card C ) & ex C being finite Coloring of R st card C = it2 & ( for C being finite Coloring of R holds it2 <= card C ) implies it1 = it2 )
assume that
A5: ex C being finite Coloring of R st card C = it1 and
A6: for C being finite Coloring of R holds it1 <= card C and
A7: ex C being finite Coloring of R st card C = it2 and
A8: for C being finite Coloring of R holds it2 <= card C ; ::_thesis: it1 = it2
consider C1 being finite Coloring of R such that
A9: card C1 = it1 by A5;
consider C2 being finite Coloring of R such that
A10: card C2 = it2 by A7;
( it1 <= card C2 & it2 <= card C1 ) by A6, A8;
hence it1 = it2 by A9, A10, XXREAL_0:1; ::_thesis: verum
end;
end;
:: 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 ) ) );
registration
let R be empty RelStr ;
cluster chromatic# R -> empty ;
coherence
chromatic# R is empty
proof
consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
C is empty by EQREL_1:32;
hence chromatic# R is empty by A1; ::_thesis: verum
end;
end;
registration
let R be non empty with_finite_chromatic# RelStr ;
cluster chromatic# R -> positive ;
coherence
chromatic# R is positive
proof
ex C being finite Coloring of R st card C = chromatic# R by Def3;
hence chromatic# R is positive ; ::_thesis: verum
end;
end;
definition
let R be RelStr ;
attrR is with_finite_cliquecover# means :Def4: :: MYCIELSK:def 4
ex C being Clique-partition of R st C is finite ;
end;
:: 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 );
registration
cluster with_finite_cliquecover# for RelStr ;
existence
ex b1 being RelStr st b1 is with_finite_cliquecover#
proof
take R = the empty RelStr ; ::_thesis: R is with_finite_cliquecover#
reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
reconsider S = S as Clique-partition of R ;
take S ; :: according to MYCIELSK:def_4 ::_thesis: S is finite
thus S is finite ; ::_thesis: verum
end;
end;
registration
cluster finite -> with_finite_cliquecover# for RelStr ;
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_cliquecover#
proof
let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_cliquecover# )
set cR = the carrier of R;
assume A1: R is finite ; ::_thesis: R is with_finite_cliquecover#
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: R is with_finite_cliquecover#
then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
for x being set st x in S holds
x is Clique of R ;
then reconsider S = S as Clique-partition of R by DILWORTH:def_11;
take S ; :: according to MYCIELSK:def_4 ::_thesis: S is finite
thus S is finite ; ::_thesis: verum
end;
supposeA2: not R is empty ; ::_thesis: R is with_finite_cliquecover#
reconsider cRp1 = the carrier of R as non empty finite set by A2, A1;
set S = SmallestPartition the carrier of R;
deffunc H1( set ) -> set = {c1};
defpred S1[ set ] means verum;
A3: SmallestPartition the carrier of R = { H1(x) where x is Element of cRp1 : S1[x] } by EQREL_1:37;
A4: { H1(x) where x is Element of cRp1 : S1[x] } is finite from PRE_CIRC:sch_1();
now__::_thesis:_for_z_being_set_st_z_in_SmallestPartition_the_carrier_of_R_holds_
z_is_Clique_of_R
let z be set ; ::_thesis: ( z in SmallestPartition the carrier of R implies z is Clique of R )
assume A5: z in SmallestPartition the carrier of R ; ::_thesis: z is Clique of R
ex x being Element of the carrier of R st z = {x} by A5, A3;
hence z is Clique of R by A2, SUBSET_1:33; ::_thesis: verum
end;
then reconsider S = SmallestPartition the carrier of R as Clique-partition of R by DILWORTH:def_11;
take S ; :: according to MYCIELSK:def_4 ::_thesis: S is finite
thus S is finite by A4; ::_thesis: verum
end;
end;
end;
end;
registration
let R be with_finite_cliquecover# RelStr ;
cluster finite V89() Clique-wise for a_partition of the carrier of R;
existence
ex b1 being Clique-partition of R st b1 is finite by Def4;
end;
registration
let R be with_finite_cliquecover# RelStr ;
let S be Subset of R;
cluster subrelstr S -> with_finite_cliquecover# ;
coherence
subrelstr S is with_finite_cliquecover#
proof
set sS = subrelstr S;
consider C being Clique-partition of R such that
A1: C is finite by Def4;
A2: the carrier of (subrelstr S) = S by YELLOW_0:def_15;
reconsider CS = C | S as a_partition of S ;
for x being set st x in CS holds
x is Clique of (subrelstr S)
proof
let x be set ; ::_thesis: ( x in CS implies x is Clique of (subrelstr S) )
assume x in CS ; ::_thesis: x is Clique of (subrelstr S)
then consider X being Element of C such that
A3: x = X /\ S and
A4: X meets S ;
ex y being set st
( y in X & y in S ) by A4, XBOOLE_0:3;
then X is Clique of R by DILWORTH:def_11;
hence x is Clique of (subrelstr S) by A3, DILWORTH:29; ::_thesis: verum
end;
then CS is Clique-partition of (subrelstr S) by A2, DILWORTH:def_11;
hence subrelstr S is with_finite_cliquecover# by A1, Def4; ::_thesis: verum
end;
end;
definition
let R be with_finite_cliquecover# RelStr ;
func cliquecover# R -> Nat means :Def5: :: MYCIELSK:def 5
( ex C being finite Clique-partition of R st card C = it & ( for C being finite Clique-partition of R holds it <= card C ) );
existence
ex b1 being Nat st
( ex C being finite Clique-partition of R st card C = b1 & ( for C being finite Clique-partition of R holds b1 <= card C ) )
proof
defpred S1[ Nat] means ex C being finite Clique-partition of R st card C = $1;
consider C being Clique-partition of R such that
A1: C is finite by Def4;
card C = card C ;
then A2: ex k being Nat st S1[k] by A1;
consider n being Nat such that
A3: S1[n] and
A4: for k being Nat st S1[k] holds
n <= k from NAT_1:sch_5(A2);
take n ; ::_thesis: ( ex C being finite Clique-partition of R st card C = n & ( for C being finite Clique-partition of R holds n <= card C ) )
thus ex C being finite Clique-partition of R st card C = n by A3; ::_thesis: for C being finite Clique-partition of R holds n <= card C
let C be finite Clique-partition of R; ::_thesis: n <= card C
thus n <= card C by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Nat st ex C being finite Clique-partition of R st card C = b1 & ( for C being finite Clique-partition of R holds b1 <= card C ) & ex C being finite Clique-partition of R st card C = b2 & ( for C being finite Clique-partition of R holds b2 <= card C ) holds
b1 = b2
proof
let it1, it2 be Nat; ::_thesis: ( ex C being finite Clique-partition of R st card C = it1 & ( for C being finite Clique-partition of R holds it1 <= card C ) & ex C being finite Clique-partition of R st card C = it2 & ( for C being finite Clique-partition of R holds it2 <= card C ) implies it1 = it2 )
assume that
A5: ex C being finite Clique-partition of R st card C = it1 and
A6: for C being finite Clique-partition of R holds it1 <= card C and
A7: ex C being finite Clique-partition of R st card C = it2 and
A8: for C being finite Clique-partition of R holds it2 <= card C ; ::_thesis: it1 = it2
consider C1 being finite Clique-partition of R such that
A9: card C1 = it1 by A5;
consider C2 being finite Clique-partition of R such that
A10: card C2 = it2 by A7;
( it1 <= card C2 & it2 <= card C1 ) by A6, A8;
hence it1 = it2 by A9, A10, XXREAL_0:1; ::_thesis: verum
end;
end;
:: 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 ) ) );
registration
let R be empty RelStr ;
cluster cliquecover# R -> empty ;
coherence
cliquecover# R is empty
proof
consider C being finite Clique-partition of R such that
A1: card C = cliquecover# R by Def5;
C is empty by EQREL_1:32;
hence cliquecover# R is empty by A1; ::_thesis: verum
end;
end;
registration
let R be non empty with_finite_cliquecover# RelStr ;
cluster cliquecover# R -> positive ;
coherence
cliquecover# R is positive
proof
consider C being finite Clique-partition of R such that
A1: card C = cliquecover# R by Def5;
thus cliquecover# R is positive by A1; ::_thesis: verum
end;
end;
theorem Th11: :: MYCIELSK:11
for R being finite RelStr holds clique# R <= card the carrier of R
proof
let R be finite RelStr ; ::_thesis: clique# R <= card the carrier of R
consider C being finite Clique of R such that
A1: card C = clique# R by DILWORTH:def_4;
card C c= card the carrier of R by CARD_1:11;
hence clique# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum
end;
theorem :: MYCIELSK:12
for R being finite RelStr holds stability# R <= card the carrier of R
proof
let R be finite RelStr ; ::_thesis: stability# R <= card the carrier of R
consider C being finite StableSet of R such that
A1: card C = stability# R by DILWORTH:def_6;
card C c= card the carrier of R by CARD_1:11;
hence stability# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum
end;
theorem Th13: :: MYCIELSK:13
for R being finite RelStr holds chromatic# R <= card the carrier of R
proof
let R be finite RelStr ; ::_thesis: chromatic# R <= card the carrier of R
consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
card C c= card the carrier of R by Th7;
hence chromatic# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum
end;
theorem :: MYCIELSK:14
for R being finite RelStr holds cliquecover# R <= card the carrier of R
proof
let R be finite RelStr ; ::_thesis: cliquecover# R <= card the carrier of R
consider C being finite Clique-partition of R such that
A1: card C = cliquecover# R by Def5;
card C c= card the carrier of R by Th7;
hence cliquecover# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum
end;
theorem Th15: :: MYCIELSK:15
for R being with_finite_clique# with_finite_chromatic# RelStr holds clique# R <= chromatic# R
proof
let P be with_finite_clique# with_finite_chromatic# RelStr ; ::_thesis: clique# P <= chromatic# P
assume A1: clique# P > chromatic# P ; ::_thesis: contradiction
consider A being Clique of P such that
A2: card A = clique# P by DILWORTH:def_4;
consider C being finite Coloring of P such that
A3: card C = chromatic# P by Def3;
( card (card C) = card C & card (card A) = card A ) ;
then A4: card C in card A by A3, A1, A2, NAT_1:41;
set cP = the carrier of P;
percases ( P is empty or not P is empty ) ;
suppose P is empty ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
supposeA5: not P is empty ; ::_thesis: contradiction
defpred S1[ set , set ] means ( $1 in A & $2 in C & $1 in $2 );
A6: for x being set st x in A holds
ex y being set st
( y in C & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in A implies ex y being set st
( y in C & S1[x,y] ) )
assume A7: x in A ; ::_thesis: ex y being set st
( y in C & S1[x,y] )
then reconsider xp1 = x as Element of P ;
not the carrier of P is empty by A5;
then xp1 in the carrier of P ;
then x in union C by EQREL_1:def_4;
then consider y being set such that
A8: x in y and
A9: y in C by TARSKI:def_4;
take y ; ::_thesis: ( y in C & S1[x,y] )
thus ( y in C & S1[x,y] ) by A7, A8, A9; ::_thesis: verum
end;
consider f being Function of A,C such that
A10: for x being set st x in A holds
S1[x,f . x] from FUNCT_2:sch_1(A6);
consider x, y being set such that
A11: x in A and
A12: y in A and
A13: x <> y and
A14: f . x = f . y by A5, A4, FINSEQ_4:65;
f . x in C by A11, FUNCT_2:5;
then A15: f . x is StableSet of P by DILWORTH:def_12;
( x in f . x & y in f . x ) by A14, A11, A12, A10;
hence contradiction by A15, A11, A12, A13, DILWORTH:15; ::_thesis: verum
end;
end;
end;
theorem :: MYCIELSK:16
for R being with_finite_stability# with_finite_cliquecover# RelStr holds stability# R <= cliquecover# R
proof
let R be with_finite_stability# with_finite_cliquecover# RelStr ; ::_thesis: stability# R <= cliquecover# R
assume A1: stability# R > cliquecover# R ; ::_thesis: contradiction
consider A being StableSet of R such that
A2: card A = stability# R by DILWORTH:def_6;
consider C being finite Clique-partition of R such that
A3: card C = cliquecover# R by Def5;
( card (card C) = card C & card (card A) = card A ) ;
then A4: card C in card A by A3, A1, A2, NAT_1:41;
set cR = the carrier of R;
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
supposeA5: not R is empty ; ::_thesis: contradiction
defpred S1[ set , set ] means ( $1 in A & $2 in C & $1 in $2 );
A6: for x being set st x in A holds
ex y being set st
( y in C & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in A implies ex y being set st
( y in C & S1[x,y] ) )
assume A7: x in A ; ::_thesis: ex y being set st
( y in C & S1[x,y] )
reconsider xp1 = x as Element of R by A7;
not the carrier of R is empty by A5;
then xp1 in the carrier of R ;
then x in union C by EQREL_1:def_4;
then consider y being set such that
A8: x in y and
A9: y in C by TARSKI:def_4;
take y ; ::_thesis: ( y in C & S1[x,y] )
thus ( y in C & S1[x,y] ) by A7, A8, A9; ::_thesis: verum
end;
consider f being Function of A,C such that
A10: for x being set st x in A holds
S1[x,f . x] from FUNCT_2:sch_1(A6);
consider x, y being set such that
A11: x in A and
A12: y in A and
A13: x <> y and
A14: f . x = f . y by A5, A4, FINSEQ_4:65;
f . x in C by A11, FUNCT_2:5;
then A15: f . x is Clique of R by DILWORTH:def_11;
( x in f . x & y in f . x ) by A14, A11, A12, A10;
hence contradiction by A15, A11, A12, A13, DILWORTH:15; ::_thesis: verum
end;
end;
end;
begin
theorem Th17: :: MYCIELSK:17
for R being RelStr
for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds
not a <= b
proof
let R be RelStr ; ::_thesis: for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds
not a <= b
let x, y be Element of R; ::_thesis: for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds
not a <= b
let a, b be Element of (ComplRelStr R); ::_thesis: ( x = a & y = b & x <= y implies not a <= b )
assume that
A1: x = a and
A2: y = b ; ::_thesis: ( not x <= y or not a <= b )
set cR = the carrier of R;
set iR = the InternalRel of R;
set CR = ComplRelStr R;
set iCR = the InternalRel of (ComplRelStr R);
A3: the InternalRel of (ComplRelStr R) = ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def_8;
assume x <= y ; ::_thesis: not a <= b
then [x,y] in the InternalRel of R by ORDERS_2:def_5;
then not [x,y] in the InternalRel of R ` by XBOOLE_0:def_5;
then not [x,y] in the InternalRel of (ComplRelStr R) by A3, XBOOLE_0:def_5;
hence not a <= b by A1, A2, ORDERS_2:def_5; ::_thesis: verum
end;
theorem Th18: :: MYCIELSK:18
for R being RelStr
for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds
x <= y
proof
let R be RelStr ; ::_thesis: for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds
x <= y
let x, y be Element of R; ::_thesis: for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds
x <= y
let a, b be Element of (ComplRelStr R); ::_thesis: ( x = a & y = b & x <> y & x in the carrier of R & not a <= b implies x <= y )
assume that
A1: x = a and
A2: y = b and
A3: x <> y and
A4: x in the carrier of R ; ::_thesis: ( a <= b or x <= y )
set cR = the carrier of R;
set iR = the InternalRel of R;
set CR = ComplRelStr R;
set iCR = the InternalRel of (ComplRelStr R);
A5: the InternalRel of (ComplRelStr R) = ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def_8;
A6: [x,y] in [: the carrier of R, the carrier of R:] by A4, ZFMISC_1:def_2;
assume not a <= b ; ::_thesis: x <= y
then A7: not [x,y] in the InternalRel of (ComplRelStr R) by A1, A2, ORDERS_2:def_5;
not [x,y] in id the carrier of R by A3, RELAT_1:def_10;
then not [x,y] in the InternalRel of R ` by A5, A7, XBOOLE_0:def_5;
then [x,y] in the InternalRel of R by A6, XBOOLE_0:def_5;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
registration
let R be finite RelStr ;
cluster ComplRelStr R -> finite ;
coherence
ComplRelStr R is finite
proof
the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8;
hence ComplRelStr R is finite ; ::_thesis: verum
end;
end;
theorem Th19: :: MYCIELSK:19
for R being symmetric RelStr
for C being Clique of R holds C is StableSet of (ComplRelStr R)
proof
let R be symmetric RelStr ; ::_thesis: for C being Clique of R holds C is StableSet of (ComplRelStr R)
let C be Clique of R; ::_thesis: C is StableSet of (ComplRelStr R)
now__::_thesis:_for_x,_y_being_Element_of_(ComplRelStr_R)_st_x_in_C_&_y_in_C_&_x_<>_y_holds_
(_not_x_<=_y_&_not_y_<=_x_)
let x, y be Element of (ComplRelStr R); ::_thesis: ( x in C & y in C & x <> y implies ( not x <= y & not y <= x ) )
assume that
A1: x in C and
A2: y in C and
A3: x <> y ; ::_thesis: ( not x <= y & not y <= x )
reconsider a = x, b = y as Element of R by NECKLACE:def_8;
( a <= b or b <= a ) by A1, A2, A3, DILWORTH:6;
then ( a <= b & b <= a ) by Th6;
hence ( not x <= y & not y <= x ) by Th17; ::_thesis: verum
end;
hence C is StableSet of (ComplRelStr R) by DILWORTH:def_2, NECKLACE:def_8; ::_thesis: verum
end;
theorem Th20: :: MYCIELSK:20
for R being symmetric RelStr
for C being Clique of (ComplRelStr R) holds C is StableSet of R
proof
let R be symmetric RelStr ; ::_thesis: for C being Clique of (ComplRelStr R) holds C is StableSet of R
let C be Clique of (ComplRelStr R); ::_thesis: C is StableSet of R
now__::_thesis:_for_x,_y_being_Element_of_R_st_x_in_C_&_y_in_C_&_x_<>_y_holds_
(_not_x_<=_y_&_not_y_<=_x_)
let x, y be Element of R; ::_thesis: ( x in C & y in C & x <> y implies ( not x <= y & not y <= x ) )
assume that
A1: x in C and
A2: y in C and
A3: x <> y ; ::_thesis: ( not x <= y & not y <= x )
reconsider a = x, b = y as Element of (ComplRelStr R) by NECKLACE:def_8;
( a <= b or b <= a ) by A1, A2, A3, DILWORTH:6;
then ( a <= b & b <= a ) by Th6;
hence ( not x <= y & not y <= x ) by Th17; ::_thesis: verum
end;
hence C is StableSet of R by DILWORTH:def_2, NECKLACE:def_8; ::_thesis: verum
end;
theorem Th21: :: MYCIELSK:21
for R being RelStr
for C being StableSet of R holds C is Clique of (ComplRelStr R)
proof
let R be RelStr ; ::_thesis: for C being StableSet of R holds C is Clique of (ComplRelStr R)
let C be StableSet of R; ::_thesis: C is Clique of (ComplRelStr R)
set CR = ComplRelStr R;
A1: C is Subset of (ComplRelStr R) by NECKLACE:def_8;
now__::_thesis:_for_a,_b_being_Element_of_(ComplRelStr_R)_st_a_in_C_&_b_in_C_&_a_<>_b_&_not_a_<=_b_holds_
b_<=_a
let a, b be Element of (ComplRelStr R); ::_thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a )
assume that
A2: a in C and
A3: b in C and
A4: a <> b ; ::_thesis: ( a <= b or b <= a )
reconsider ap1 = a, bp1 = b as Element of R by NECKLACE:def_8;
( not ap1 <= bp1 & not bp1 <= ap1 ) by A2, A3, A4, DILWORTH:def_2;
hence ( a <= b or b <= a ) by A2, A4, Th18; ::_thesis: verum
end;
hence C is Clique of (ComplRelStr R) by A1, DILWORTH:6; ::_thesis: verum
end;
theorem Th22: :: MYCIELSK:22
for R being RelStr
for C being StableSet of (ComplRelStr R) holds C is Clique of R
proof
let R be RelStr ; ::_thesis: for C being StableSet of (ComplRelStr R) holds C is Clique of R
let C be StableSet of (ComplRelStr R); ::_thesis: C is Clique of R
A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_C_&_b_in_C_&_a_<>_b_&_not_a_<=_b_holds_
b_<=_a
let a, b be Element of R; ::_thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a )
assume that
A2: a in C and
A3: b in C and
A4: a <> b ; ::_thesis: ( a <= b or b <= a )
reconsider ap1 = a, bp1 = b as Element of (ComplRelStr R) by NECKLACE:def_8;
( not ap1 <= bp1 & not bp1 <= ap1 ) by A2, A3, A4, DILWORTH:def_2;
hence ( a <= b or b <= a ) by A4, A2, A1, Th18; ::_thesis: verum
end;
hence C is Clique of R by DILWORTH:6, NECKLACE:def_8; ::_thesis: verum
end;
registration
let R be with_finite_clique# RelStr ;
cluster ComplRelStr R -> with_finite_stability# ;
coherence
ComplRelStr R is with_finite_stability#
proof
set CR = ComplRelStr R;
consider C being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card C by DILWORTH:def_3;
assume not ComplRelStr R is with_finite_stability# ; ::_thesis: contradiction
then A2: for A being finite StableSet of (ComplRelStr R) ex B being finite StableSet of (ComplRelStr R) st card B > card A by DILWORTH:def_5;
defpred S1[ Nat] means ex S being finite StableSet of (ComplRelStr R) st card S > R;
consider B being finite StableSet of (ComplRelStr R) such that
A3: card B > card ({} (ComplRelStr R)) by A2;
A4: S1[ 0 ] by A3;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then consider S being finite StableSet of (ComplRelStr R) such that
A6: card S > n ;
consider T being finite StableSet of (ComplRelStr R) such that
A7: card T > card S by A2;
card S >= n + 1 by A6, NAT_1:13;
then card T > n + 1 by A7, XXREAL_0:2;
hence S1[n + 1] ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5);
then consider S being finite StableSet of (ComplRelStr R) such that
A8: card S > card C ;
S is Clique of R by Th22;
hence contradiction by A1, A8; ::_thesis: verum
end;
end;
registration
let R be symmetric with_finite_stability# RelStr ;
cluster ComplRelStr R -> with_finite_clique# ;
coherence
ComplRelStr R is with_finite_clique#
proof
set CR = ComplRelStr R;
consider C being finite StableSet of R such that
A1: for D being finite StableSet of R holds card D <= card C by DILWORTH:def_5;
assume not ComplRelStr R is with_finite_clique# ; ::_thesis: contradiction
then A2: for C being finite Clique of (ComplRelStr R) ex D being finite Clique of (ComplRelStr R) st card D > card C by DILWORTH:def_3;
defpred S1[ Nat] means ex S being finite Clique of (ComplRelStr R) st card S > R;
consider B being finite Clique of (ComplRelStr R) such that
A3: card B > card ({} (ComplRelStr R)) by A2;
A4: S1[ 0 ] by A3;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then consider S being finite Clique of (ComplRelStr R) such that
A6: card S > n ;
consider T being finite Clique of (ComplRelStr R) such that
A7: card T > card S by A2;
card S >= n + 1 by A6, NAT_1:13;
then card T > n + 1 by A7, XXREAL_0:2;
hence S1[n + 1] ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5);
then consider S being finite Clique of (ComplRelStr R) such that
A8: card S > card C ;
S is StableSet of R by Th20;
hence contradiction by A1, A8; ::_thesis: verum
end;
end;
theorem Th23: :: MYCIELSK:23
for R being symmetric with_finite_clique# RelStr holds clique# R = stability# (ComplRelStr R)
proof
let R be symmetric with_finite_clique# RelStr ; ::_thesis: clique# R = stability# (ComplRelStr R)
set k = stability# (ComplRelStr R);
consider A being finite StableSet of (ComplRelStr R) such that
A1: card A = stability# (ComplRelStr R) by DILWORTH:def_6;
A is Clique of R by Th22;
then A2: ex C being finite Clique of R st card C = stability# (ComplRelStr R) by A1;
now__::_thesis:_for_T_being_finite_Clique_of_R_holds_card_T_<=_stability#_(ComplRelStr_R)
let T be finite Clique of R; ::_thesis: card T <= stability# (ComplRelStr R)
T is StableSet of (ComplRelStr R) by Th19;
hence card T <= stability# (ComplRelStr R) by DILWORTH:def_6; ::_thesis: verum
end;
hence clique# R = stability# (ComplRelStr R) by A2, DILWORTH:def_4; ::_thesis: verum
end;
theorem :: MYCIELSK:24
for R being symmetric with_finite_stability# RelStr holds stability# R = clique# (ComplRelStr R)
proof
let R be symmetric with_finite_stability# RelStr ; ::_thesis: stability# R = clique# (ComplRelStr R)
set CR = ComplRelStr R;
set k = clique# (ComplRelStr R);
consider A being finite Clique of (ComplRelStr R) such that
A1: card A = clique# (ComplRelStr R) by DILWORTH:def_4;
A is StableSet of R by Th20;
then A2: ex C being finite StableSet of R st card C = clique# (ComplRelStr R) by A1;
now__::_thesis:_for_T_being_finite_StableSet_of_R_holds_card_T_<=_clique#_(ComplRelStr_R)
let T be finite StableSet of R; ::_thesis: card T <= clique# (ComplRelStr R)
T is Clique of (ComplRelStr R) by Th21;
hence card T <= clique# (ComplRelStr R) by DILWORTH:def_4; ::_thesis: verum
end;
hence stability# R = clique# (ComplRelStr R) by A2, DILWORTH:def_6; ::_thesis: verum
end;
theorem Th25: :: MYCIELSK:25
for R being RelStr
for C being Coloring of R holds C is Clique-partition of (ComplRelStr R)
proof
let R be RelStr ; ::_thesis: for C being Coloring of R holds C is Clique-partition of (ComplRelStr R)
let C be Coloring of R; ::_thesis: C is Clique-partition of (ComplRelStr R)
A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8;
now__::_thesis:_for_x_being_set_st_x_in_C_holds_
x_is_Clique_of_(ComplRelStr_R)
let x be set ; ::_thesis: ( x in C implies x is Clique of (ComplRelStr R) )
assume x in C ; ::_thesis: x is Clique of (ComplRelStr R)
then x is StableSet of R by DILWORTH:def_12;
hence x is Clique of (ComplRelStr R) by Th21; ::_thesis: verum
end;
hence C is Clique-partition of (ComplRelStr R) by A1, DILWORTH:def_11; ::_thesis: verum
end;
theorem Th26: :: MYCIELSK:26
for R being symmetric RelStr
for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R
proof
let R be symmetric RelStr ; ::_thesis: for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R
let C be Clique-partition of (ComplRelStr R); ::_thesis: C is Coloring of R
set CR = ComplRelStr R;
A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8;
now__::_thesis:_for_x_being_set_st_x_in_C_holds_
x_is_StableSet_of_R
let x be set ; ::_thesis: ( x in C implies x is StableSet of R )
assume x in C ; ::_thesis: x is StableSet of R
then x is Clique of (ComplRelStr R) by DILWORTH:def_11;
hence x is StableSet of R by Th20; ::_thesis: verum
end;
hence C is Coloring of R by A1, DILWORTH:def_12; ::_thesis: verum
end;
theorem Th27: :: MYCIELSK:27
for R being symmetric RelStr
for C being Clique-partition of R holds C is Coloring of (ComplRelStr R)
proof
let R be symmetric RelStr ; ::_thesis: for C being Clique-partition of R holds C is Coloring of (ComplRelStr R)
let C be Clique-partition of R; ::_thesis: C is Coloring of (ComplRelStr R)
set CR = ComplRelStr R;
A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8;
now__::_thesis:_for_x_being_set_st_x_in_C_holds_
x_is_StableSet_of_(ComplRelStr_R)
let x be set ; ::_thesis: ( x in C implies x is StableSet of (ComplRelStr R) )
assume x in C ; ::_thesis: x is StableSet of (ComplRelStr R)
then x is Clique of R by DILWORTH:def_11;
hence x is StableSet of (ComplRelStr R) by Th19; ::_thesis: verum
end;
hence C is Coloring of (ComplRelStr R) by A1, DILWORTH:def_12; ::_thesis: verum
end;
theorem Th28: :: MYCIELSK:28
for R being RelStr
for C being Coloring of (ComplRelStr R) holds C is Clique-partition of R
proof
let R be RelStr ; ::_thesis: for C being Coloring of (ComplRelStr R) holds C is Clique-partition of R
let C be Coloring of (ComplRelStr R); ::_thesis: C is Clique-partition of R
set CR = ComplRelStr R;
A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8;
now__::_thesis:_for_x_being_set_st_x_in_C_holds_
x_is_Clique_of_R
let x be set ; ::_thesis: ( x in C implies x is Clique of R )
assume x in C ; ::_thesis: x is Clique of R
then x is StableSet of (ComplRelStr R) by DILWORTH:def_12;
hence x is Clique of R by Th22; ::_thesis: verum
end;
hence C is Clique-partition of R by A1, DILWORTH:def_11; ::_thesis: verum
end;
registration
let R be with_finite_chromatic# RelStr ;
cluster ComplRelStr R -> with_finite_cliquecover# ;
coherence
ComplRelStr R is with_finite_cliquecover#
proof
consider C being Coloring of R such that
A1: C is finite by Def2;
C is Clique-partition of (ComplRelStr R) by Th25;
hence ComplRelStr R is with_finite_cliquecover# by A1, Def4; ::_thesis: verum
end;
end;
registration
let R be symmetric with_finite_cliquecover# RelStr ;
cluster ComplRelStr R -> with_finite_chromatic# ;
coherence
ComplRelStr R is with_finite_chromatic#
proof
consider C being Clique-partition of R such that
A1: C is finite by Def4;
C is Coloring of (ComplRelStr R) by Th27;
hence ComplRelStr R is with_finite_chromatic# by A1, Def2; ::_thesis: verum
end;
end;
theorem Th29: :: MYCIELSK:29
for R being symmetric with_finite_chromatic# RelStr holds chromatic# R = cliquecover# (ComplRelStr R)
proof
let R be symmetric with_finite_chromatic# RelStr ; ::_thesis: chromatic# R = cliquecover# (ComplRelStr R)
set CR = ComplRelStr R;
set k = cliquecover# (ComplRelStr R);
consider C being finite Clique-partition of (ComplRelStr R) such that
A1: card C = cliquecover# (ComplRelStr R) by Def5;
C is Coloring of R by Th26;
then A2: ex C being finite Coloring of R st card C = cliquecover# (ComplRelStr R) by A1;
now__::_thesis:_for_C_being_finite_Coloring_of_R_holds_not_cliquecover#_(ComplRelStr_R)_>_card_C
let C be finite Coloring of R; ::_thesis: not cliquecover# (ComplRelStr R) > card C
assume A3: cliquecover# (ComplRelStr R) > card C ; ::_thesis: contradiction
C is Clique-partition of (ComplRelStr R) by Th25;
hence contradiction by A3, Def5; ::_thesis: verum
end;
hence chromatic# R = cliquecover# (ComplRelStr R) by A2, Def3; ::_thesis: verum
end;
theorem :: MYCIELSK:30
for R being symmetric with_finite_cliquecover# RelStr holds cliquecover# R = chromatic# (ComplRelStr R)
proof
let R be symmetric with_finite_cliquecover# RelStr ; ::_thesis: cliquecover# R = chromatic# (ComplRelStr R)
set CR = ComplRelStr R;
set k = chromatic# (ComplRelStr R);
consider C being finite Coloring of (ComplRelStr R) such that
A1: card C = chromatic# (ComplRelStr R) by Def3;
C is Clique-partition of R by Th28;
then A2: ex C being finite Clique-partition of R st card C = chromatic# (ComplRelStr R) by A1;
now__::_thesis:_for_C_being_finite_Clique-partition_of_R_holds_not_chromatic#_(ComplRelStr_R)_>_card_C
let C be finite Clique-partition of R; ::_thesis: not chromatic# (ComplRelStr R) > card C
assume A3: chromatic# (ComplRelStr R) > card C ; ::_thesis: contradiction
C is Coloring of (ComplRelStr R) by Th27;
hence contradiction by A3, Def3; ::_thesis: verum
end;
hence cliquecover# R = chromatic# (ComplRelStr R) by A2, Def5; ::_thesis: verum
end;
begin
definition
let R be RelStr ;
let v be Element of R;
func Adjacent v -> Subset of R means :Def6: :: MYCIELSK:def 6
for x being Element of R holds
( x in it iff ( x < v or v < x ) );
existence
ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff ( x < v or v < x ) )
proof
set D = { x where x is Element of R : ( x < v or v < x ) } ;
set cR = the carrier of R;
set iR = the InternalRel of R;
{ x where x is Element of R : ( x < v or v < x ) } c= the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of R : ( x < v or v < x ) } or x in the carrier of R )
assume x in { x where x is Element of R : ( x < v or v < x ) } ; ::_thesis: x in the carrier of R
then consider a being Element of R such that
A1: x = a and
A2: ( a < v or v < a ) ;
percases ( a < v or v < a ) by A2;
suppose a < v ; ::_thesis: x in the carrier of R
then a <= v by ORDERS_2:def_6;
then [a,v] in the InternalRel of R by ORDERS_2:def_5;
then [a,v] in [: the carrier of R, the carrier of R:] ;
hence x in the carrier of R by A1, ZFMISC_1:87; ::_thesis: verum
end;
suppose v < a ; ::_thesis: x in the carrier of R
then v <= a by ORDERS_2:def_6;
then [v,a] in the InternalRel of R by ORDERS_2:def_5;
then [v,a] in [: the carrier of R, the carrier of R:] ;
hence x in the carrier of R by A1, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;
then reconsider D = { x where x is Element of R : ( x < v or v < x ) } as Subset of R ;
take D ; ::_thesis: for x being Element of R holds
( x in D iff ( x < v or v < x ) )
let x be Element of R; ::_thesis: ( x in D iff ( x < v or v < x ) )
hereby ::_thesis: ( ( x < v or v < x ) implies x in D )
assume x in D ; ::_thesis: ( x < v or v < x )
then consider a being Element of R such that
A3: x = a and
A4: ( a < v or v < a ) ;
thus ( x < v or v < x ) by A3, A4; ::_thesis: verum
end;
assume ( x < v or v < x ) ; ::_thesis: x in D
hence x in D ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of R st ( for x being Element of R holds
( x in b1 iff ( x < v or v < x ) ) ) & ( for x being Element of R holds
( x in b2 iff ( x < v or v < x ) ) ) holds
b1 = b2
proof
let it1, it2 be Subset of R; ::_thesis: ( ( for x being Element of R holds
( x in it1 iff ( x < v or v < x ) ) ) & ( for x being Element of R holds
( x in it2 iff ( x < v or v < x ) ) ) implies it1 = it2 )
assume that
A5: for x being Element of R holds
( x in it1 iff ( x < v or v < x ) ) and
A6: for x being Element of R holds
( x in it2 iff ( x < v or v < x ) ) ; ::_thesis: it1 = it2
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: it2 c= it1
let x be set ; ::_thesis: ( x in it1 implies x in it2 )
assume A7: x in it1 ; ::_thesis: x in it2
then reconsider xp1 = x as Element of R ;
( xp1 < v or v < xp1 ) by A5, A7;
hence x in it2 by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in it2 or x in it1 )
assume A8: x in it2 ; ::_thesis: x in it1
then reconsider xp1 = x as Element of R ;
( xp1 < v or v < xp1 ) by A6, A8;
hence x in it1 by A5; ::_thesis: verum
end;
end;
:: 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: :: MYCIELSK:31
for R being with_finite_chromatic# RelStr
for C being finite Coloring of R
for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
proof
let R be with_finite_chromatic# RelStr ; ::_thesis: for C being finite Coloring of R
for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
let C be finite Coloring of R; ::_thesis: for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
let c be set ; ::_thesis: ( c in C & card C = chromatic# R implies ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) ) )
assume that
A1: c in C and
A2: card C = chromatic# R ; ::_thesis: ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
assume A3: for v being Element of R holds
( not v in c or ex d being Element of C st
( d <> c & ( for w being Element of R holds
( not w in Adjacent v or not w in d ) ) ) ) ; ::_thesis: contradiction
set cR = the carrier of R;
A4: union C = the carrier of R by EQREL_1:def_4;
reconsider c = c as Subset of the carrier of R by A1;
A5: c <> {} by A1, EQREL_1:def_4;
set Cc = C \ {c};
A6: c in {c} by TARSKI:def_1;
percases ( C \ {c} is empty or not C \ {c} is empty ) ;
supposeA7: C \ {c} is empty ; ::_thesis: contradiction
consider v being set such that
A8: v in c by A5, XBOOLE_0:def_1;
reconsider v = v as Element of R by A8;
consider d being Element of C such that
A9: d <> c and
for w being Element of R holds
( not w in Adjacent v or not w in d ) by A8, A3;
0 = (card C) - (card {c}) by A1, A7, CARD_1:27, EULER_1:4;
then 0 + 1 = ((card C) - 1) + 1 by CARD_1:30;
then consider x being set such that
A10: C = {x} by CARD_2:42;
( c = x & d = x ) by A1, A10, TARSKI:def_1;
hence contradiction by A9; ::_thesis: verum
end;
suppose not C \ {c} is empty ; ::_thesis: contradiction
then reconsider Cc = C \ {c} as non empty set ;
defpred S1[ set , set ] means for vv being Element of the carrier of R st $1 = vv holds
( $2 <> c & $2 in C & ( for w being Element of R holds
( not w in Adjacent vv or not w in $2 ) ) );
A11: for e being set st e in c holds
ex u being set st S1[e,u]
proof
let v be set ; ::_thesis: ( v in c implies ex u being set st S1[v,u] )
assume A12: v in c ; ::_thesis: ex u being set st S1[v,u]
reconsider vv = v as Element of the carrier of R by A12;
consider d being Element of C such that
A13: d <> c and
A14: for w being Element of R holds
( not w in Adjacent vv or not w in d ) by A12, A3;
take d ; ::_thesis: S1[v,d]
thus S1[v,d] by A13, A14, A1; ::_thesis: verum
end;
consider r being Function such that
A15: dom r = c and
A16: for e being set st e in c holds
S1[e,r . e] from CLASSES1:sch_1(A11);
defpred S2[ set ] means verum;
deffunc H1( set ) -> set = $1 \/ (r " {$1});
reconsider Cc = Cc as non empty finite set ;
set D = { H1(d) where d is Element of Cc : S2[d] } ;
consider d being set such that
A17: d in Cc by XBOOLE_0:def_1;
A18: d \/ (r " {d}) in { H1(d) where d is Element of Cc : S2[d] } by A17;
A19: { H1(d) where d is Element of Cc : S2[d] } c= bool the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(d) where d is Element of Cc : S2[d] } or x in bool the carrier of R )
assume x in { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: x in bool the carrier of R
then consider d being Element of Cc such that
A20: x = d \/ (r " {d}) ;
A21: r " {d} c= c by A15, RELAT_1:132;
A22: r " {d} c= the carrier of R by A21, XBOOLE_1:1;
d in C by XBOOLE_0:def_5;
then x c= the carrier of R by A20, A22, XBOOLE_1:8;
hence x in bool the carrier of R ; ::_thesis: verum
end;
A23: union { H1(d) where d is Element of Cc : S2[d] } = the carrier of R
proof
thus union { H1(d) where d is Element of Cc : S2[d] } c= the carrier of R :: according to XBOOLE_0:def_10 ::_thesis: the carrier of R c= union { H1(d) where d is Element of Cc : S2[d] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { H1(d) where d is Element of Cc : S2[d] } or x in the carrier of R )
assume x in union { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: x in the carrier of R
then consider Y being set such that
A24: x in Y and
A25: Y in { H1(d) where d is Element of Cc : S2[d] } by TARSKI:def_4;
thus x in the carrier of R by A24, A25, A19; ::_thesis: verum
end;
thus the carrier of R c= union { H1(d) where d is Element of Cc : S2[d] } ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in union { H1(d) where d is Element of Cc : S2[d] } )
assume A26: x in the carrier of R ; ::_thesis: x in union { H1(d) where d is Element of Cc : S2[d] }
then consider d being set such that
A27: x in d and
A28: d in C by A4, TARSKI:def_4;
reconsider xp1 = x as Element of the carrier of R by A26;
percases ( d = c or d <> c ) ;
supposeA29: d = c ; ::_thesis: x in union { H1(d) where d is Element of Cc : S2[d] }
then r . xp1 <> c by A27, A16;
then A30: not r . xp1 in {c} by TARSKI:def_1;
r . xp1 in C by A27, A29, A16;
then A31: r . xp1 in Cc by A30, XBOOLE_0:def_5;
r . xp1 in {(r . xp1)} by TARSKI:def_1;
then x in r " {(r . xp1)} by A27, A29, A15, FUNCT_1:def_7;
then A32: x in (r . xp1) \/ (r " {(r . xp1)}) by XBOOLE_0:def_3;
(r . xp1) \/ (r " {(r . xp1)}) in { H1(d) where d is Element of Cc : S2[d] } by A31;
hence x in union { H1(d) where d is Element of Cc : S2[d] } by A32, TARSKI:def_4; ::_thesis: verum
end;
suppose d <> c ; ::_thesis: x in union { H1(d) where d is Element of Cc : S2[d] }
then not d in {c} by TARSKI:def_1;
then d in Cc by A28, XBOOLE_0:def_5;
then A33: d \/ (r " {d}) in { H1(d) where d is Element of Cc : S2[d] } ;
x in d \/ (r " {d}) by A27, XBOOLE_0:def_3;
hence x in union { H1(d) where d is Element of Cc : S2[d] } by A33, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
end;
A34: for A being Subset of the carrier of R st A in { H1(d) where d is Element of Cc : S2[d] } holds
( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) )
proof
let A be Subset of the carrier of R; ::_thesis: ( A in { H1(d) where d is Element of Cc : S2[d] } implies ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) ) )
assume A in { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) )
then consider da being Element of Cc such that
A35: A = da \/ (r " {da}) ;
A36: da in C by XBOOLE_0:def_5;
then not da is empty by EQREL_1:def_4;
hence A <> {} by A35; ::_thesis: for B being Subset of the carrier of R holds
( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B )
let B be Subset of the carrier of R; ::_thesis: ( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B )
assume B in { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: ( A = B or A misses B )
then consider db being Element of Cc such that
A37: B = db \/ (r " {db}) ;
A38: db in C by XBOOLE_0:def_5;
percases ( da = db or da <> db ) ;
suppose da = db ; ::_thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A35, A37; ::_thesis: verum
end;
supposeA39: da <> db ; ::_thesis: ( A = B or A misses B )
then A40: da misses db by A36, A38, EQREL_1:def_4;
A41: r " {da} misses r " {db} by A39, FUNCT_1:71, ZFMISC_1:11;
assume A <> B ; ::_thesis: A misses B
assume A meets B ; ::_thesis: contradiction
then consider x being set such that
A42: x in A and
A43: x in B by XBOOLE_0:3;
percases ( ( x in da & x in db ) or ( x in da & x in r " {db} ) or ( x in r " {da} & x in db ) or ( x in r " {da} & x in r " {db} ) ) by A42, A43, A35, A37, XBOOLE_0:def_3;
suppose ( x in da & x in db ) ; ::_thesis: contradiction
hence contradiction by A40, XBOOLE_0:3; ::_thesis: verum
end;
supposethat A44: x in da and
A45: x in r " {db} ; ::_thesis: contradiction
A46: da <> c by A6, XBOOLE_0:def_5;
r " {db} c= c by A15, RELAT_1:132;
then da meets c by A44, A45, XBOOLE_0:3;
hence contradiction by A46, A36, A1, EQREL_1:def_4; ::_thesis: verum
end;
supposethat A47: x in r " {da} and
A48: x in db ; ::_thesis: contradiction
A49: db <> c by A6, XBOOLE_0:def_5;
r " {da} c= c by A15, RELAT_1:132;
then db meets c by A47, A48, XBOOLE_0:3;
hence contradiction by A49, A38, A1, EQREL_1:def_4; ::_thesis: verum
end;
suppose ( x in r " {da} & x in r " {db} ) ; ::_thesis: contradiction
hence contradiction by A41, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
end;
end;
reconsider D = { H1(d) where d is Element of Cc : S2[d] } as a_partition of the carrier of R by A19, A23, A34, EQREL_1:def_4;
now__::_thesis:_for_x_being_set_st_x_in_D_holds_
x_is_StableSet_of_R
let x be set ; ::_thesis: ( x in D implies x is StableSet of R )
assume A50: x in D ; ::_thesis: x is StableSet of R
then reconsider S = x as Subset of R ;
consider d being Element of Cc such that
A51: x = d \/ (r " {d}) by A50;
A52: r " {d} c= c by A15, RELAT_1:132;
A53: d in C by XBOOLE_0:def_5;
A54: d is StableSet of R by A53, DILWORTH:def_12;
A55: c is StableSet of R by A1, DILWORTH:def_12;
S is stable
proof
let a, b be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( not a in S or not b in S or a = b or ( not a <= b & not b <= a ) )
assume that
A56: a in S and
A57: b in S and
A58: a <> b ; ::_thesis: ( not a <= b & not b <= a )
percases ( ( a in d & b in d ) or ( a in d & b in r " {d} ) or ( a in r " {d} & b in d ) or ( a in r " {d} & b in r " {d} ) ) by A56, A57, A51, XBOOLE_0:def_3;
suppose ( a in d & b in d ) ; ::_thesis: ( not a <= b & not b <= a )
hence ( not a <= b & not b <= a ) by A54, A58, DILWORTH:def_2; ::_thesis: verum
end;
supposethat A59: a in d and
A60: b in r " {d} ; ::_thesis: ( not a <= b & not b <= a )
r . b in {d} by A60, FUNCT_1:def_7;
then r . b = d by TARSKI:def_1;
then not a in Adjacent b by A59, A52, A60, A16;
then ( not a < b & not b < a ) by Def6;
hence ( not a <= b & not b <= a ) by A58, ORDERS_2:def_6; ::_thesis: verum
end;
supposethat A61: a in r " {d} and
A62: b in d ; ::_thesis: ( not a <= b & not b <= a )
r . a in {d} by A61, FUNCT_1:def_7;
then r . a = d by TARSKI:def_1;
then not b in Adjacent a by A62, A52, A61, A16;
then ( not a < b & not b < a ) by Def6;
hence ( not a <= b & not b <= a ) by A58, ORDERS_2:def_6; ::_thesis: verum
end;
suppose ( a in r " {d} & b in r " {d} ) ; ::_thesis: ( not a <= b & not b <= a )
hence ( not a <= b & not b <= a ) by A52, A55, A58, DILWORTH:def_2; ::_thesis: verum
end;
end;
end;
hence x is StableSet of R ; ::_thesis: verum
end;
then reconsider D = D as Coloring of R by DILWORTH:def_12;
card Cc = (card C) - (card {c}) by A1, EULER_1:4;
then (card Cc) + 1 = ((card C) - 1) + 1 by CARD_1:30;
then A63: card Cc < card C by NAT_1:13;
deffunc H2( set ) -> set = $1 \/ (r " {$1});
consider s being Function such that
A64: dom s = Cc and
A65: for x being set st x in Cc holds
s . x = H2(x) from FUNCT_1:sch_3();
A66: rng s c= D
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in D )
assume y in rng s ; ::_thesis: y in D
then consider d being set such that
A67: d in dom s and
A68: y = s . d by FUNCT_1:def_3;
y = d \/ (r " {d}) by A64, A65, A67, A68;
hence y in D by A67, A64; ::_thesis: verum
end;
then reconsider s = s as Function of Cc,D by A64, FUNCT_2:2;
A69: s is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom s or not x2 in dom s or not s . x1 = s . x2 or x1 = x2 )
assume that
A70: x1 in dom s and
A71: x2 in dom s and
A72: s . x1 = s . x2 ; ::_thesis: x1 = x2
A73: s . x1 = x1 \/ (r " {x1}) by A70, A65;
A74: s . x2 = x2 \/ (r " {x2}) by A71, A65;
thus x1 c= x2 :: according to XBOOLE_0:def_10 ::_thesis: x2 c= x1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x1 or x in x2 )
assume A75: x in x1 ; ::_thesis: x in x2
then A76: x in s . x1 by A73, XBOOLE_0:def_3;
percases ( x in x2 or x in r " {x2} ) by A76, A72, A74, XBOOLE_0:def_3;
suppose x in x2 ; ::_thesis: x in x2
hence x in x2 ; ::_thesis: verum
end;
supposeA77: x in r " {x2} ; ::_thesis: x in x2
A78: r " {x2} c= dom r by RELAT_1:132;
A79: x1 in C by A70, XBOOLE_0:def_5;
then reconsider x1 = x1 as Subset of the carrier of R ;
x1 meets c by A78, A77, A15, A75, XBOOLE_0:3;
then x1 = c by A79, A1, EQREL_1:def_4;
hence x in x2 by A6, A70, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
thus x2 c= x1 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x2 or x in x1 )
assume A80: x in x2 ; ::_thesis: x in x1
then A81: x in s . x2 by A74, XBOOLE_0:def_3;
percases ( x in x1 or x in r " {x1} ) by A81, A72, A73, XBOOLE_0:def_3;
suppose x in x1 ; ::_thesis: x in x1
hence x in x1 ; ::_thesis: verum
end;
supposeA82: x in r " {x1} ; ::_thesis: x in x1
A83: r " {x1} c= dom r by RELAT_1:132;
A84: x2 in C by A71, XBOOLE_0:def_5;
then reconsider x2 = x2 as Subset of the carrier of R ;
x2 meets c by A83, A82, A15, A80, XBOOLE_0:3;
then x2 = c by A84, A1, EQREL_1:def_4;
hence x in x1 by A6, A71, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
end;
D c= rng s
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in rng s )
assume x in D ; ::_thesis: x in rng s
then consider d being Element of Cc such that
A85: x = d \/ (r " {d}) ;
s . d = d \/ (r " {d}) by A65;
hence x in rng s by A85, A64, FUNCT_1:def_3; ::_thesis: verum
end;
then D = rng s by A66, XBOOLE_0:def_10;
then s is onto by FUNCT_2:def_3;
then A86: card Cc = card D by A69, A18, EULER_1:11;
then D is finite ;
hence contradiction by A63, A86, A2, Def3; ::_thesis: verum
end;
end;
end;
begin
definition
let n be Nat;
mode NatRelStr of n -> strict RelStr means :Def7: :: MYCIELSK:def 7
the carrier of it = n;
existence
ex b1 being strict RelStr st the carrier of b1 = n
proof
reconsider I = {} as Relation of n,n by RELSET_1:12;
take RelStr(# n,I #) ; ::_thesis: the carrier of RelStr(# n,I #) = n
thus the carrier of RelStr(# n,I #) = n ; ::_thesis: verum
end;
end;
:: 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 );
registration
cluster -> empty for NatRelStr of 0 ;
coherence
for b1 being NatRelStr of 0 holds b1 is empty by Def7;
end;
registration
let n be non empty Nat;
cluster -> non empty for NatRelStr of n;
coherence
for b1 being NatRelStr of n holds not b1 is empty by Def7;
end;
registration
let n be Nat;
cluster -> finite for NatRelStr of n;
coherence
for b1 being NatRelStr of n holds b1 is finite by Def7;
cluster strict irreflexive for NatRelStr of n;
existence
ex b1 being NatRelStr of n st b1 is irreflexive
proof
reconsider I = {} as Relation of n,n by RELSET_1:12;
set R = RelStr(# n,I #);
reconsider R = RelStr(# n,I #) as NatRelStr of n by Def7;
R is irreflexive
proof
let x be set ; :: according to NECKLACE:def_5 ::_thesis: ( not x in the carrier of R or not [x,x] in the InternalRel of R )
assume x in the carrier of R ; ::_thesis: not [x,x] in the InternalRel of R
thus not [x,x] in the InternalRel of R ; ::_thesis: verum
end;
hence ex b1 being NatRelStr of n st b1 is irreflexive ; ::_thesis: verum
end;
end;
definition
let n be Nat;
func CompleteRelStr n -> NatRelStr of n means :Def8: :: MYCIELSK:def 8
the InternalRel of it = [:n,n:] \ (id n);
existence
ex b1 being NatRelStr of n st the InternalRel of b1 = [:n,n:] \ (id n)
proof
[:n,n:] c= [:n,n:] ;
then reconsider f = [:n,n:] as Relation of n ;
reconsider R = RelStr(# n,(f \ (id n)) #) as NatRelStr of n by Def7;
take R ; ::_thesis: the InternalRel of R = [:n,n:] \ (id n)
thus the InternalRel of R = [:n,n:] \ (id n) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being NatRelStr of n st the InternalRel of b1 = [:n,n:] \ (id n) & the InternalRel of b2 = [:n,n:] \ (id n) holds
b1 = b2
proof
let C1, C2 be NatRelStr of n; ::_thesis: ( the InternalRel of C1 = [:n,n:] \ (id n) & the InternalRel of C2 = [:n,n:] \ (id n) implies C1 = C2 )
( the carrier of C1 = n & the carrier of C2 = n ) by Def7;
hence ( the InternalRel of C1 = [:n,n:] \ (id n) & the InternalRel of C2 = [:n,n:] \ (id n) implies C1 = C2 ) ; ::_thesis: verum
end;
end;
:: 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: :: MYCIELSK:32
for n being Nat
for x, y being set st x in n & y in n holds
( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )
proof
let n be Nat; ::_thesis: for x, y being set st x in n & y in n holds
( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )
let x, y be set ; ::_thesis: ( x in n & y in n implies ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y ) )
assume A1: ( x in n & y in n ) ; ::_thesis: ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )
hereby ::_thesis: ( x <> y implies [x,y] in the InternalRel of (CompleteRelStr n) )
assume [x,y] in the InternalRel of (CompleteRelStr n) ; ::_thesis: x <> y
then [x,y] in [:n,n:] \ (id n) by Def8;
then not [x,y] in id n by XBOOLE_0:def_5;
hence x <> y by A1, RELAT_1:def_10; ::_thesis: verum
end;
assume x <> y ; ::_thesis: [x,y] in the InternalRel of (CompleteRelStr n)
then ( [x,y] in [:n,n:] & not [x,y] in id n ) by A1, RELAT_1:def_10, ZFMISC_1:87;
then [x,y] in [:n,n:] \ (id n) by XBOOLE_0:def_5;
hence [x,y] in the InternalRel of (CompleteRelStr n) by Def8; ::_thesis: verum
end;
registration
let n be Nat;
cluster CompleteRelStr n -> symmetric irreflexive ;
coherence
( CompleteRelStr n is irreflexive & CompleteRelStr n is symmetric )
proof
set R = CompleteRelStr n;
set cR = the carrier of (CompleteRelStr n);
set iR = the InternalRel of (CompleteRelStr n);
A1: the carrier of (CompleteRelStr n) = n by Def7;
thus CompleteRelStr n is irreflexive ::_thesis: CompleteRelStr n is symmetric
proof
let x be set ; :: according to NECKLACE:def_5 ::_thesis: ( not x in the carrier of (CompleteRelStr n) or not [x,x] in the InternalRel of (CompleteRelStr n) )
assume x in the carrier of (CompleteRelStr n) ; ::_thesis: not [x,x] in the InternalRel of (CompleteRelStr n)
hence not [x,x] in the InternalRel of (CompleteRelStr n) by A1, Th32; ::_thesis: verum
end;
thus CompleteRelStr n is symmetric ::_thesis: verum
proof
let x, y be set ; :: according to RELAT_2:def_3,NECKLACE:def_3 ::_thesis: ( not x in the carrier of (CompleteRelStr n) or not y in the carrier of (CompleteRelStr n) or not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
assume ( x in the carrier of (CompleteRelStr n) & y in the carrier of (CompleteRelStr n) ) ; ::_thesis: ( not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
then A2: ( x in n & y in n ) by Def7;
assume [x,y] in the InternalRel of (CompleteRelStr n) ; ::_thesis: [y,x] in the InternalRel of (CompleteRelStr n)
hence [y,x] in the InternalRel of (CompleteRelStr n) by A2, Th32; ::_thesis: verum
end;
end;
end;
registration
let n be Nat;
cluster [#] (CompleteRelStr n) -> clique ;
coherence
[#] (CompleteRelStr n) is connected
proof
set R = CompleteRelStr n;
set iR = the InternalRel of (CompleteRelStr n);
let x, y be set ; :: according to RELAT_2:def_6,DILWORTH:def_1 ::_thesis: ( not x in [#] (CompleteRelStr n) or not y in [#] (CompleteRelStr n) or x = y or [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
assume ( x in [#] (CompleteRelStr n) & y in [#] (CompleteRelStr n) ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
then A1: ( x in n & y in n ) by Def7;
assume x <> y ; ::_thesis: ( [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
hence ( [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) ) by A1, Th32; ::_thesis: verum
end;
end;
theorem Th33: :: MYCIELSK:33
for n being Nat holds clique# (CompleteRelStr n) = n
proof
let n be Nat; ::_thesis: clique# (CompleteRelStr n) = n
set R = CompleteRelStr n;
A1: card (card n) = card n ;
[#] (CompleteRelStr n) = n by Def7;
then A2: ex C being finite Clique of (CompleteRelStr n) st card C = n by A1, CARD_1:40;
for T being finite Clique of (CompleteRelStr n) holds card T <= n
proof
let T be finite Clique of (CompleteRelStr n); ::_thesis: card T <= n
card n = n by A1, CARD_1:40;
then A3: card the carrier of (CompleteRelStr n) = n by Def7;
A4: card T <= clique# (CompleteRelStr n) by DILWORTH:def_4;
clique# (CompleteRelStr n) <= n by A3, Th11;
hence card T <= n by A4, XXREAL_0:2; ::_thesis: verum
end;
hence clique# (CompleteRelStr n) = n by A2, DILWORTH:def_4; ::_thesis: verum
end;
theorem :: MYCIELSK:34
for n being non empty Nat holds stability# (CompleteRelStr n) = 1
proof
let n be non empty Nat; ::_thesis: stability# (CompleteRelStr n) = 1
set R = CompleteRelStr n;
[#] (CompleteRelStr n) is Clique of (CompleteRelStr n) ;
hence stability# (CompleteRelStr n) = 1 by DILWORTH:20; ::_thesis: verum
end;
theorem Th35: :: MYCIELSK:35
for n being Nat holds chromatic# (CompleteRelStr n) = n
proof
let n be Nat; ::_thesis: chromatic# (CompleteRelStr n) = n
set R = CompleteRelStr n;
clique# (CompleteRelStr n) = n by Th33;
then A1: n <= chromatic# (CompleteRelStr n) by Th15;
A2: chromatic# (CompleteRelStr n) <= card the carrier of (CompleteRelStr n) by Th13;
card (card n) = card n ;
then card n = n by CARD_1:40;
then card the carrier of (CompleteRelStr n) = n by Def7;
hence chromatic# (CompleteRelStr n) = n by A1, A2, XXREAL_0:1; ::_thesis: verum
end;
theorem :: MYCIELSK:36
for n being non empty Nat holds cliquecover# (CompleteRelStr n) = 1
proof
let n be non empty Nat; ::_thesis: cliquecover# (CompleteRelStr n) = 1
set R = CompleteRelStr n;
set cR = the carrier of (CompleteRelStr n);
reconsider C = { the carrier of (CompleteRelStr n)} as a_partition of the carrier of (CompleteRelStr n) by EQREL_1:39;
A1: now__::_thesis:_for_x_being_set_st_x_in_C_holds_
x_is_Clique_of_(CompleteRelStr_n)
let x be set ; ::_thesis: ( x in C implies x is Clique of (CompleteRelStr n) )
assume x in C ; ::_thesis: x is Clique of (CompleteRelStr n)
then x = [#] (CompleteRelStr n) by TARSKI:def_1;
hence x is Clique of (CompleteRelStr n) ; ::_thesis: verum
end;
A2: now__::_thesis:_ex_C_being_a_partition_of_the_carrier_of_(CompleteRelStr_n)_st_
(_C_is_finite_&_C_is_Clique-partition_of_(CompleteRelStr_n)_&_card_C_=_1_)
take C = C; ::_thesis: ( C is finite & C is Clique-partition of (CompleteRelStr n) & card C = 1 )
thus C is finite ; ::_thesis: ( C is Clique-partition of (CompleteRelStr n) & card C = 1 )
thus C is Clique-partition of (CompleteRelStr n) by A1, DILWORTH:def_11; ::_thesis: card C = 1
thus card C = 1 by CARD_1:30; ::_thesis: verum
end;
now__::_thesis:_for_C_being_finite_Clique-partition_of_(CompleteRelStr_n)_holds_1_<=_card_C
let C be finite Clique-partition of (CompleteRelStr n); ::_thesis: 1 <= card C
0 + 1 <= card C by NAT_1:13;
hence 1 <= card C ; ::_thesis: verum
end;
hence cliquecover# (CompleteRelStr n) = 1 by A2, Def5; ::_thesis: verum
end;
begin
definition
let n be Nat;
let R be NatRelStr of n;
func Mycielskian R -> NatRelStr of (2 * n) + 1 means :Def9: :: MYCIELSK:def 9
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)}:]
proof
set cR = the carrier of R;
set iR = the InternalRel of R;
set cMR = (2 * n) + 1;
set iMR = ((( 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)}:];
A1: the carrier of R = n by Def7;
n <= n + n by NAT_1:11;
then A2: n < (2 * n) + 1 by NAT_1:13;
((( 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)}:] c= [:((2 * n) + 1),((2 * n) + 1):]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ((( 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)}:] or z in [:((2 * n) + 1),((2 * n) + 1):] )
assume A3: z in ((( 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)}:] ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):]
percases ( z in the InternalRel of R or z in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or z in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or z in [:{(2 * n)},((2 * n) \ n):] or z in [:((2 * n) \ n),{(2 * n)}:] ) by A3, Th4;
suppose z in the InternalRel of R ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):]
then consider c, d being set such that
A4: c in the carrier of R and
A5: d in the carrier of R and
A6: z = [c,d] by ZFMISC_1:def_2;
reconsider c = c, d = d as Nat by A1, A4, A5, NECKLACE:3;
( c < n & d < n ) by A1, A4, A5, NAT_1:44;
then ( c < (2 * n) + 1 & d < (2 * n) + 1 ) by A2, XXREAL_0:2;
then ( c in (2 * n) + 1 & d in (2 * n) + 1 ) by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A6, ZFMISC_1:def_2; ::_thesis: verum
end;
suppose z in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):]
then consider x, y being Element of NAT such that
A7: z = [x,(y + n)] and
A8: [x,y] in the InternalRel of R ;
x in the carrier of R by A8, ZFMISC_1:87;
then x < n by A1, NAT_1:44;
then x < (2 * n) + 1 by A2, XXREAL_0:2;
then A9: x in (2 * n) + 1 by NAT_1:44;
y in the carrier of R by A8, ZFMISC_1:87;
then y < n by A1, NAT_1:44;
then y + n < n + n by XREAL_1:6;
then y + n < (2 * n) + 1 by NAT_1:13;
then y + n in (2 * n) + 1 by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A7, A9, ZFMISC_1:def_2; ::_thesis: verum
end;
suppose z in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):]
then consider x, y being Element of NAT such that
A10: z = [(x + n),y] and
A11: [x,y] in the InternalRel of R ;
y in the carrier of R by A11, ZFMISC_1:87;
then y < n by A1, NAT_1:44;
then y < (2 * n) + 1 by A2, XXREAL_0:2;
then A12: y in (2 * n) + 1 by NAT_1:44;
x in the carrier of R by A11, ZFMISC_1:87;
then x < n by A1, NAT_1:44;
then x + n < n + n by XREAL_1:6;
then x + n < (2 * n) + 1 by NAT_1:13;
then x + n in (2 * n) + 1 by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A10, A12, ZFMISC_1:def_2; ::_thesis: verum
end;
suppose z in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):]
then consider c, d being set such that
A13: c in {(2 * n)} and
A14: d in (2 * n) \ n and
A15: z = [c,d] by ZFMISC_1:def_2;
A16: c = 2 * n by A13, TARSKI:def_1;
reconsider c = c as Nat by A13, TARSKI:def_1;
c < (2 * n) + 1 by A16, NAT_1:13;
then A17: c in (2 * n) + 1 by NAT_1:44;
reconsider d = d as Nat by A14, NECKLACE:3;
d < 2 * n by A14, Th2;
then d < (2 * n) + 1 by NAT_1:13;
then d in (2 * n) + 1 by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A17, A15, ZFMISC_1:def_2; ::_thesis: verum
end;
suppose z in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):]
then consider c, d being set such that
A18: c in (2 * n) \ n and
A19: d in {(2 * n)} and
A20: z = [c,d] by ZFMISC_1:def_2;
A21: d = 2 * n by A19, TARSKI:def_1;
reconsider d = d as Nat by A19, TARSKI:def_1;
d < (2 * n) + 1 by A21, NAT_1:13;
then A22: d in (2 * n) + 1 by NAT_1:44;
reconsider c = c as Nat by A18, NECKLACE:3;
c < 2 * n by A18, Th2;
then c < (2 * n) + 1 by NAT_1:13;
then c in (2 * n) + 1 by NAT_1:44;
hence z in [:((2 * n) + 1),((2 * n) + 1):] by A22, A20, ZFMISC_1:def_2; ::_thesis: verum
end;
end;
end;
then reconsider iMR = ((( 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)}:] as Relation of ((2 * n) + 1) ;
set MR = RelStr(# ((2 * n) + 1),iMR #);
take RelStr(# ((2 * n) + 1),iMR #) ; ::_thesis: ( RelStr(# ((2 * n) + 1),iMR #) is NatRelStr of (2 * n) + 1 & the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( 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)}:] )
thus the carrier of RelStr(# ((2 * n) + 1),iMR #) = (2 * n) + 1 ; :: according to MYCIELSK:def_7 ::_thesis: the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( 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)}:]
thus the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( 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)}:] ; ::_thesis: verum
end;
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
proof
let A, B be NatRelStr of (2 * n) + 1; ::_thesis: ( the InternalRel of A = ((( 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 B = ((( 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)}:] implies A = B )
( the carrier of A = (2 * n) + 1 & the carrier of B = (2 * n) + 1 ) by Def7;
hence ( the InternalRel of A = ((( 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 B = ((( 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)}:] implies A = B ) ; ::_thesis: verum
end;
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: :: MYCIELSK:37
for n being Nat
for R being NatRelStr of n holds the carrier of R c= the carrier of (Mycielskian R)
proof
let n be Nat; ::_thesis: for R being NatRelStr of n holds the carrier of R c= the carrier of (Mycielskian R)
let R be NatRelStr of n; ::_thesis: the carrier of R c= the carrier of (Mycielskian R)
A1: the carrier of R = n by Def7;
n <= n + n by NAT_1:12;
then n <= (2 * n) + 1 by NAT_1:12;
then n c= (2 * n) + 1 by NAT_1:39;
hence the carrier of R c= the carrier of (Mycielskian R) by A1, Def7; ::_thesis: verum
end;
theorem Th38: :: MYCIELSK:38
for n being Nat
for R being NatRelStr of n
for x, y being Nat holds
( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) )
proof
let n be Nat; ::_thesis: for R being NatRelStr of n
for x, y being Nat holds
( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) )
let R be NatRelStr of n; ::_thesis: for x, y being Nat holds
( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) )
let a, b be Nat; ::_thesis: ( not [a,b] in the InternalRel of (Mycielskian R) or ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) )
set cR = the carrier of R;
set iR = the InternalRel of R;
defpred S1[] means [a,b] in the InternalRel of (Mycielskian R);
defpred S2[] means ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) );
A1: the InternalRel of (Mycielskian R) = ((( 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)}:] by Def9;
assume A2: S1[] ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) )
percases ( [a,b] in the InternalRel of R or [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in [:{(2 * n)},((2 * n) \ n):] or [a,b] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A1, Th4;
suppose [a,b] in the InternalRel of R ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) )
then ( a in the carrier of R & b in the carrier of R ) by ZFMISC_1:87;
then ( a in n & b in n ) by Def7;
hence S2[] by NAT_1:44; ::_thesis: verum
end;
suppose [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) )
then consider x, y being Element of NAT such that
A3: [x,(y + n)] = [a,b] and
A4: [x,y] in the InternalRel of R ;
y in the carrier of R by A4, ZFMISC_1:87;
then y in n by Def7;
then y < n by NAT_1:44;
then A5: y + n < n + n by XREAL_1:6;
x in the carrier of R by A4, ZFMISC_1:87;
then x in n by Def7;
then x < n by NAT_1:44;
hence S2[] by A5, A3, XTUPLE_0:1; ::_thesis: verum
end;
suppose [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) )
then consider x, y being Element of NAT such that
A6: [(x + n),y] = [a,b] and
A7: [x,y] in the InternalRel of R ;
x in the carrier of R by A7, ZFMISC_1:87;
then x in n by Def7;
then x < n by NAT_1:44;
then A8: x + n < n + n by XREAL_1:6;
y in the carrier of R by A7, ZFMISC_1:87;
then y in n by Def7;
then y < n by NAT_1:44;
hence S2[] by A8, A6, XTUPLE_0:1; ::_thesis: verum
end;
supposeA9: [a,b] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) )
A10: b in (2 * n) \ n by A9, ZFMISC_1:87;
a in {(2 * n)} by A9, ZFMISC_1:87;
hence S2[] by A10, Th2, TARSKI:def_1; ::_thesis: verum
end;
supposeA11: [a,b] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) )
A12: a in (2 * n) \ n by A11, ZFMISC_1:87;
b in {(2 * n)} by A11, ZFMISC_1:87;
hence S2[] by A12, Th2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
theorem Th39: :: MYCIELSK:39
for n being Nat
for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R)
proof
let n be Nat; ::_thesis: for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R)
let R be NatRelStr of n; ::_thesis: the InternalRel of R c= the InternalRel of (Mycielskian R)
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
the InternalRel of (Mycielskian R) = ((( 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)}:] by Def9;
hence the InternalRel of R c= the InternalRel of (Mycielskian R) by Th3; ::_thesis: verum
end;
theorem Th40: :: MYCIELSK:40
for n being Nat
for R being NatRelStr of n
for x, y being set st x in n & y in n & [x,y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
proof
let n be Nat; ::_thesis: for R being NatRelStr of n
for x, y being set st x in n & y in n & [x,y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let R be NatRelStr of n; ::_thesis: for x, y being set st x in n & y in n & [x,y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let a, b be set ; ::_thesis: ( a in n & b in n & [a,b] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R )
assume that
A1: a in n and
A2: b in n and
A3: [a,b] in the InternalRel of (Mycielskian R) ; ::_thesis: [a,b] in the InternalRel of R
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
A4: the InternalRel of (Mycielskian R) = ((( 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)}:] by Def9;
percases ( [a,b] in the InternalRel of R or [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in [:{(2 * n)},((2 * n) \ n):] or [a,b] in [:((2 * n) \ n),{(2 * n)}:] ) by A3, A4, Th4;
suppose [a,b] in the InternalRel of R ; ::_thesis: [a,b] in the InternalRel of R
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R
then consider x, y being Element of NAT such that
A5: [a,b] = [x,(y + n)] and
[x,y] in the InternalRel of R ;
b = y + n by A5, XTUPLE_0:1;
then y + n < n by A2, NAT_1:44;
then y < n - n by XREAL_1:20;
then y < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R
then consider x, y being Element of NAT such that
A6: [a,b] = [(x + n),y] and
[x,y] in the InternalRel of R ;
a = x + n by A6, XTUPLE_0:1;
then x + n < n by A1, NAT_1:44;
then x < n - n by XREAL_1:20;
then x < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [a,b] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: [a,b] in the InternalRel of R
then consider c, d being set such that
A7: c in {(2 * n)} and
d in (2 * n) \ n and
A8: [a,b] = [c,d] by ZFMISC_1:def_2;
A9: c = 2 * n by A7, TARSKI:def_1;
A10: c = a by A8, XTUPLE_0:1;
n + n < n by A1, A10, A9, NAT_1:44;
then n < n - n by XREAL_1:20;
then n < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [a,b] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: [a,b] in the InternalRel of R
then consider c, d being set such that
c in (2 * n) \ n and
A11: d in {(2 * n)} and
A12: [a,b] = [c,d] by ZFMISC_1:def_2;
A13: d = 2 * n by A11, TARSKI:def_1;
A14: d = b by A12, XTUPLE_0:1;
n + n < n by A2, A14, A13, NAT_1:44;
then n < n - n by XREAL_1:20;
then n < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
end;
end;
theorem Th41: :: MYCIELSK:41
for n being Nat
for R being NatRelStr of n
for x, y being Nat st [x,y] in the InternalRel of R holds
( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )
proof
let n be Nat; ::_thesis: for R being NatRelStr of n
for x, y being Nat st [x,y] in the InternalRel of R holds
( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )
let R be NatRelStr of n; ::_thesis: for x, y being Nat st [x,y] in the InternalRel of R holds
( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )
let a, b be Nat; ::_thesis: ( [a,b] in the InternalRel of R implies ( [a,(b + n)] in the InternalRel of (Mycielskian R) & [(a + n),b] in the InternalRel of (Mycielskian R) ) )
assume A1: [a,b] in the InternalRel of R ; ::_thesis: ( [a,(b + n)] in the InternalRel of (Mycielskian R) & [(a + n),b] in the InternalRel of (Mycielskian R) )
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
A2: the InternalRel of (Mycielskian R) = ((( 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)}:] by Def9;
reconsider ap1 = a, bp1 = b as Element of NAT by ORDINAL1:def_12;
[ap1,(bp1 + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } by A1;
hence [a,(b + n)] in the InternalRel of (Mycielskian R) by A2, Th4; ::_thesis: [(a + n),b] in the InternalRel of (Mycielskian R)
[(ap1 + n),bp1] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } by A1;
hence [(a + n),b] in the InternalRel of (Mycielskian R) by A2, Th4; ::_thesis: verum
end;
theorem Th42: :: MYCIELSK:42
for n being Nat
for R being NatRelStr of n
for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
proof
let n be Nat; ::_thesis: for R being NatRelStr of n
for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let R be NatRelStr of n; ::_thesis: for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let a, b be Nat; ::_thesis: ( a in n & [a,(b + n)] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R )
set cR = the carrier of R;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
assume that
A1: a in n and
A2: [a,(b + n)] in the InternalRel of (Mycielskian R) ; ::_thesis: [a,b] in the InternalRel of R
A3: the InternalRel of (Mycielskian R) = ((( 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)}:] by Def9;
percases ( [a,(b + n)] in the InternalRel of R or [a,(b + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,(b + n)] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,(b + n)] in [:{(2 * n)},((2 * n) \ n):] or [a,(b + n)] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A3, Th4;
suppose [a,(b + n)] in the InternalRel of R ; ::_thesis: [a,b] in the InternalRel of R
then b + n in the carrier of R by ZFMISC_1:87;
then b + n in n by Def7;
then b + n < n by NAT_1:44;
then b < n - n by XREAL_1:20;
then b < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [a,(b + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R
then consider x, y being Element of NAT such that
A4: [a,(b + n)] = [x,(y + n)] and
A5: [x,y] in the InternalRel of R ;
b + n = y + n by A4, XTUPLE_0:1;
hence [a,b] in the InternalRel of R by A5, A4, XTUPLE_0:1; ::_thesis: verum
end;
suppose [a,(b + n)] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R
then consider x, y being Element of NAT such that
A6: [a,(b + n)] = [(x + n),y] and
A7: [x,y] in the InternalRel of R ;
b + n = y by A6, XTUPLE_0:1;
then b + n in the carrier of R by A7, ZFMISC_1:87;
then b + n in n by Def7;
then b + n < n by NAT_1:44;
then b < n - n by XREAL_1:20;
then b < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [a,(b + n)] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: [a,b] in the InternalRel of R
then consider c, d being set such that
A8: c in {(2 * n)} and
d in (2 * n) \ n and
A9: [a,(b + n)] = [c,d] by ZFMISC_1:def_2;
A10: c = 2 * n by A8, TARSKI:def_1;
A11: c = a by A9, XTUPLE_0:1;
n + n < n by A1, A11, A10, NAT_1:44;
then n < n - n by XREAL_1:20;
then n < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [a,(b + n)] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: [a,b] in the InternalRel of R
then consider c, d being set such that
A12: c in (2 * n) \ n and
d in {(2 * n)} and
A13: [a,(b + n)] = [c,d] by ZFMISC_1:def_2;
c = a by A13, XTUPLE_0:1;
then n <= a by A12, Th2;
hence [a,b] in the InternalRel of R by A1, NAT_1:44; ::_thesis: verum
end;
end;
end;
theorem Th43: :: MYCIELSK:43
for n being Nat
for R being NatRelStr of n
for x, y being Nat st y in n & [(x + n),y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
proof
let n be Nat; ::_thesis: for R being NatRelStr of n
for x, y being Nat st y in n & [(x + n),y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let R be NatRelStr of n; ::_thesis: for x, y being Nat st y in n & [(x + n),y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
let a, b be Nat; ::_thesis: ( b in n & [(a + n),b] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R )
set cR = the carrier of R;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
assume that
A1: b in n and
A2: [(a + n),b] in the InternalRel of (Mycielskian R) ; ::_thesis: [a,b] in the InternalRel of R
A3: the InternalRel of (Mycielskian R) = ((( 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)}:] by Def9;
percases ( [(a + n),b] in the InternalRel of R or [(a + n),b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [(a + n),b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [(a + n),b] in [:{(2 * n)},((2 * n) \ n):] or [(a + n),b] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A3, Th4;
suppose [(a + n),b] in the InternalRel of R ; ::_thesis: [a,b] in the InternalRel of R
then a + n in the carrier of R by ZFMISC_1:87;
then a + n in n by Def7;
then a + n < n by NAT_1:44;
then a < n - n by XREAL_1:20;
then a < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [(a + n),b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R
then consider x, y being Element of NAT such that
A4: [(a + n),b] = [x,(y + n)] and
A5: [x,y] in the InternalRel of R ;
a + n = x by A4, XTUPLE_0:1;
then a + n in the carrier of R by A5, ZFMISC_1:87;
then a + n in n by Def7;
then a + n < n by NAT_1:44;
then a < n - n by XREAL_1:20;
then a < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
suppose [(a + n),b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R
then consider x, y being Element of NAT such that
A6: [(a + n),b] = [(x + n),y] and
A7: [x,y] in the InternalRel of R ;
a + n = x + n by A6, XTUPLE_0:1;
hence [a,b] in the InternalRel of R by A7, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose [(a + n),b] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: [a,b] in the InternalRel of R
then consider c, d being set such that
c in {(2 * n)} and
A8: d in (2 * n) \ n and
A9: [(a + n),b] = [c,d] by ZFMISC_1:def_2;
b = d by A9, XTUPLE_0:1;
then n <= b by A8, Th2;
hence [a,b] in the InternalRel of R by A1, NAT_1:44; ::_thesis: verum
end;
suppose [(a + n),b] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: [a,b] in the InternalRel of R
then consider c, d being set such that
c in (2 * n) \ n and
A10: d in {(2 * n)} and
A11: [(a + n),b] = [c,d] by ZFMISC_1:def_2;
A12: d = 2 * n by A10, TARSKI:def_1;
d = b by A11, XTUPLE_0:1;
then n + n < n by A1, A12, NAT_1:44;
then n < n - n by XREAL_1:20;
then n < 0 ;
hence [a,b] in the InternalRel of R ; ::_thesis: verum
end;
end;
end;
theorem Th44: :: MYCIELSK:44
for n being Nat
for R being NatRelStr of n
for m being Nat st n <= m & m < 2 * n holds
( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
proof
let n be Nat; ::_thesis: for R being NatRelStr of n
for m being Nat st n <= m & m < 2 * n holds
( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
let R be NatRelStr of n; ::_thesis: for m being Nat st n <= m & m < 2 * n holds
( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
let m be Nat; ::_thesis: ( n <= m & m < 2 * n implies ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) ) )
assume that
A1: n <= m and
A2: m < 2 * n ; ::_thesis: ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of (Mycielskian R);
A3: the InternalRel of (Mycielskian R) = ((( 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)}:] by Def9;
A4: m in (2 * n) \ n by A1, A2, Th2;
A5: 2 * n in {(2 * n)} by TARSKI:def_1;
then [m,(2 * n)] in [:((2 * n) \ n),{(2 * n)}:] by A4, ZFMISC_1:def_2;
hence [m,(2 * n)] in the InternalRel of (Mycielskian R) by A3, XBOOLE_0:def_3; ::_thesis: [(2 * n),m] in the InternalRel of (Mycielskian R)
[(2 * n),m] in [:{(2 * n)},((2 * n) \ n):] by A4, A5, ZFMISC_1:def_2;
hence [(2 * n),m] in the InternalRel of (Mycielskian R) by A3, Th4; ::_thesis: verum
end;
theorem Th45: :: MYCIELSK:45
for n being Nat
for R being NatRelStr of n
for S being Subset of (Mycielskian R) st S = n holds
R = subrelstr S
proof
let n be Nat; ::_thesis: for R being NatRelStr of n
for S being Subset of (Mycielskian R) st S = n holds
R = subrelstr S
let R be NatRelStr of n; ::_thesis: for S being Subset of (Mycielskian R) st S = n holds
R = subrelstr S
let S be Subset of (Mycielskian R); ::_thesis: ( S = n implies R = subrelstr S )
assume A1: S = n ; ::_thesis: R = subrelstr S
set cR = the carrier of R;
set iR = the InternalRel of R;
set sS = subrelstr S;
set csS = the carrier of (subrelstr S);
set isS = the InternalRel of (subrelstr S);
set MR = Mycielskian R;
set cMR = the carrier of (Mycielskian R);
set iMR = the InternalRel of (Mycielskian R);
A2: the carrier of R = n by Def7;
A3: the carrier of (subrelstr S) = n by A1, YELLOW_0:def_15;
A4: the InternalRel of R = the InternalRel of (subrelstr S)
proof
thus the InternalRel of R c= the InternalRel of (subrelstr S) :: according to XBOOLE_0:def_10 ::_thesis: the InternalRel of (subrelstr S) c= the InternalRel of R
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the InternalRel of R or z in the InternalRel of (subrelstr S) )
assume A5: z in the InternalRel of R ; ::_thesis: z in the InternalRel of (subrelstr S)
then consider x, y being set such that
A6: x in the carrier of R and
A7: y in the carrier of R and
A8: z = [x,y] by ZFMISC_1:def_2;
the carrier of R c= the carrier of (Mycielskian R) by Th37;
then reconsider xMR = x, yMR = y as Element of (Mycielskian R) by A6, A7;
reconsider xsS = x, ysS = y as Element of (subrelstr S) by A6, A7, Def7, A3;
the InternalRel of R c= the InternalRel of (Mycielskian R) by Th39;
then xMR <= yMR by A5, A8, ORDERS_2:def_5;
then xsS <= ysS by A3, A2, A7, YELLOW_0:60;
hence z in the InternalRel of (subrelstr S) by A8, ORDERS_2:def_5; ::_thesis: verum
end;
thus the InternalRel of (subrelstr S) c= the InternalRel of R ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the InternalRel of (subrelstr S) or z in the InternalRel of R )
assume A9: z in the InternalRel of (subrelstr S) ; ::_thesis: z in the InternalRel of R
then consider x, y being set such that
A10: x in the carrier of (subrelstr S) and
A11: y in the carrier of (subrelstr S) and
A12: z = [x,y] by ZFMISC_1:def_2;
the carrier of R c= the carrier of (Mycielskian R) by Th37;
then reconsider xMR = x, yMR = y as Element of (Mycielskian R) by A10, A11, A2, A3;
reconsider xsS = x, ysS = y as Element of (subrelstr S) by A10, A11;
xsS <= ysS by A9, A12, ORDERS_2:def_5;
then xMR <= yMR by YELLOW_0:59;
then z in the InternalRel of (Mycielskian R) by A12, ORDERS_2:def_5;
hence z in the InternalRel of R by A10, A11, A3, A12, Th40; ::_thesis: verum
end;
end;
thus R = subrelstr S by Def7, A3, A4; ::_thesis: verum
end;
theorem Th46: :: MYCIELSK:46
for n being Nat
for R being irreflexive NatRelStr of n st 2 <= clique# R holds
clique# R = clique# (Mycielskian R)
proof
let n be Nat; ::_thesis: for R being irreflexive NatRelStr of n st 2 <= clique# R holds
clique# R = clique# (Mycielskian R)
let R be irreflexive NatRelStr of n; ::_thesis: ( 2 <= clique# R implies clique# R = clique# (Mycielskian R) )
assume that
A1: 2 <= clique# R and
A2: clique# R <> clique# (Mycielskian R) ; ::_thesis: contradiction
set cR = the carrier of R;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set cMR = the carrier of (Mycielskian R);
set iMR = the InternalRel of (Mycielskian R);
set cnMR = clique# (Mycielskian R);
A3: the carrier of R = n by Def7;
A4: the carrier of R c= the carrier of (Mycielskian R) by Th37;
consider C being finite Clique of R such that
A5: card C = clique# R by DILWORTH:def_4;
n <= n + n by NAT_1:11;
then n < (2 * n) + 1 by NAT_1:13;
then n c= (2 * n) + 1 by NAT_1:39;
then reconsider S = n as Subset of (Mycielskian R) by Def7;
A6: R = subrelstr S by Th45;
then C is Clique of (Mycielskian R) by DILWORTH:28;
then card C <= clique# (Mycielskian R) by DILWORTH:def_4;
then A7: clique# R < clique# (Mycielskian R) by A2, A5, XXREAL_0:1;
then 2 < clique# (Mycielskian R) by A1, XXREAL_0:2;
then A8: 2 + 1 <= clique# (Mycielskian R) by NAT_1:13;
consider D being finite Clique of (Mycielskian R) such that
A9: card D = clique# (Mycielskian R) by DILWORTH:def_4;
percases ( D c= n or not D c= n ) ;
supposeA10: D c= n ; ::_thesis: contradiction
D /\ S is Clique of R by A6, DILWORTH:29;
then D is Clique of R by A10, XBOOLE_1:28;
hence contradiction by A9, A7, DILWORTH:def_4; ::_thesis: verum
end;
suppose not D c= n ; ::_thesis: contradiction
then consider x being set such that
A11: x in D and
A12: not x in n by TARSKI:def_3;
x in the carrier of (Mycielskian R) by A11;
then A13: x in (2 * n) + 1 by Def7;
reconsider x = x as Nat by A13, NECKLACE:3;
reconsider xp1 = x as Element of (Mycielskian R) by A11;
A14: x >= n by A12, NAT_1:44;
x < (2 * n) + 1 by A13, NAT_1:44;
then A15: x <= 2 * n by NAT_1:13;
A16: for y being set st y in D & x <> y holds
y in n
proof
let y be set ; ::_thesis: ( y in D & x <> y implies y in n )
assume that
A17: y in D and
A18: x <> y and
A19: not y in n ; ::_thesis: contradiction
y in the carrier of (Mycielskian R) by A17;
then A20: y in (2 * n) + 1 by Def7;
reconsider y = y as Nat by A20, NECKLACE:3;
reconsider yp1 = y as Element of (Mycielskian R) by A17;
A21: y >= n by A19, NAT_1:44;
y < (2 * n) + 1 by A20, NAT_1:44;
then A22: y <= 2 * n by NAT_1:13;
set DD = D \ {x,y};
{x,y} c= D by A17, A11, ZFMISC_1:32;
then A23: card (D \ {x,y}) = (card D) - (card {x,y}) by CARD_2:44;
(1 + 2) - 2 <= (card D) - 2 by A8, A9, XREAL_1:9;
then 1 <= card (D \ {x,y}) by A23, A18, CARD_2:57;
then consider z being set such that
A24: z in D \ {x,y} by CARD_1:27, XBOOLE_0:def_1;
A25: z in D by A24, XBOOLE_0:def_5;
A26: z in the carrier of (Mycielskian R) by A24;
reconsider zp1 = z as Element of (Mycielskian R) by A24;
A27: z in (2 * n) + 1 by A26, Def7;
reconsider z = z as Nat by A27, NECKLACE:3;
x in {x,y} by TARSKI:def_2;
then A28: z <> x by A24, XBOOLE_0:def_5;
y in {x,y} by TARSKI:def_2;
then A29: z <> y by A24, XBOOLE_0:def_5;
percases ( ( x < 2 * n & y < 2 * n ) or ( x < 2 * n & y = 2 * n ) or ( x = 2 * n & y < 2 * n ) or ( x = 2 * n & y = 2 * n ) ) by A15, A22, XXREAL_0:1;
supposeA30: ( x < 2 * n & y < 2 * n ) ; ::_thesis: contradiction
( xp1 <= yp1 or yp1 <= xp1 ) by A11, A17, A18, DILWORTH:6;
then ( [x,y] in the InternalRel of (Mycielskian R) or [y,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
hence contradiction by A14, A30, A21, Th38; ::_thesis: verum
end;
supposeA31: ( x < 2 * n & y = 2 * n ) ; ::_thesis: contradiction
( xp1 <= zp1 or zp1 <= xp1 ) by A28, A25, A11, DILWORTH:6;
then A32: ( [x,z] in the InternalRel of (Mycielskian R) or [z,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
( yp1 <= zp1 or zp1 <= yp1 ) by A29, A25, A17, DILWORTH:6;
then ( [y,z] in the InternalRel of (Mycielskian R) or [z,y] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
then ( n <= z & z < 2 * n ) by A31, A21, Th38;
hence contradiction by A32, A31, A14, Th38; ::_thesis: verum
end;
supposeA33: ( x = 2 * n & y < 2 * n ) ; ::_thesis: contradiction
( yp1 <= zp1 or zp1 <= yp1 ) by A29, A25, A17, DILWORTH:6;
then A34: ( [y,z] in the InternalRel of (Mycielskian R) or [z,y] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
( xp1 <= zp1 or zp1 <= xp1 ) by A28, A25, A11, DILWORTH:6;
then ( [x,z] in the InternalRel of (Mycielskian R) or [z,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
then ( n <= z & z < 2 * n ) by A33, A14, Th38;
hence contradiction by A34, A33, A21, Th38; ::_thesis: verum
end;
suppose ( x = 2 * n & y = 2 * n ) ; ::_thesis: contradiction
hence contradiction by A18; ::_thesis: verum
end;
end;
end;
A35: card (D \ {x}) = (card D) - (card {x}) by A11, EULER_1:4
.= (card D) - 1 by CARD_1:30 ;
percases ( x < 2 * n or x = 2 * n ) by A15, XXREAL_0:1;
supposeA36: x < 2 * n ; ::_thesis: contradiction
consider xx being Nat such that
A37: x = n + xx by A14, NAT_1:10;
n + xx < n + n by A36, A37;
then A38: xx < n by XREAL_1:6;
then A39: xx in n by NAT_1:44;
reconsider xxp1 = xx as Element of (Mycielskian R) by A39, A4, A3;
A40: now__::_thesis:_not_xx_in_D
assume xx in D ; ::_thesis: contradiction
then ( xp1 <= xxp1 or xxp1 <= xp1 ) by A11, A38, A14, DILWORTH:6;
then ( [x,xx] in the InternalRel of (Mycielskian R) or [xx,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
then ( [xx,xx] in the InternalRel of R or [xx,xx] in the InternalRel of R ) by A39, A37, Th42, Th43;
hence contradiction by A39, A3, NECKLACE:def_5; ::_thesis: verum
end;
set DD = (D \ {x}) \/ {xx};
(D \ {x}) \/ {xx} c= the carrier of R
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (D \ {x}) \/ {xx} or a in the carrier of R )
assume a in (D \ {x}) \/ {xx} ; ::_thesis: a in the carrier of R
then ( a in D \ {x} or a in {xx} ) by XBOOLE_0:def_3;
then ( ( a in D & not a in {x} ) or a = xx ) by TARSKI:def_1, XBOOLE_0:def_5;
then ( ( a in D & a <> x ) or a = xx ) by TARSKI:def_1;
hence a in the carrier of R by A38, A16, A3, NAT_1:44; ::_thesis: verum
end;
then reconsider DD = (D \ {x}) \/ {xx} as Subset of R ;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_DD_&_b_in_DD_&_a_<>_b_&_not_a_<=_b_holds_
b_<=_a
let a, b be Element of R; ::_thesis: ( a in DD & b in DD & a <> b & not b1 <= b2 implies b2 <= b1 )
assume that
A41: a in DD and
A42: b in DD and
A43: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
( a in D \ {x} or a in {xx} ) by A41, XBOOLE_0:def_3;
then A44: ( ( a in D & not a in {x} ) or a = xx ) by TARSKI:def_1, XBOOLE_0:def_5;
( b in D \ {x} or b in {xx} ) by A42, XBOOLE_0:def_3;
then A45: ( ( b in D & not b in {x} ) or b = xx ) by TARSKI:def_1, XBOOLE_0:def_5;
A46: ( a in the carrier of R & b in the carrier of R ) by A41;
reconsider an = a, bn = b as Nat by A41, A3, NECKLACE:3;
reconsider ap1 = a, bp1 = b as Element of (Mycielskian R) by A46, A4;
percases ( ( a in D & a <> x & b in D & b <> x ) or ( a in D & a <> x & b = xx ) or ( a = xx & b in D & b <> x ) ) by A43, A44, A45, TARSKI:def_1;
supposeA47: ( a in D & a <> x & b in D & b <> x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
( ap1 <= bp1 or bp1 <= ap1 ) by A47, A43, DILWORTH:6;
hence ( a <= b or b <= a ) by A6, A41, YELLOW_0:60; ::_thesis: verum
end;
supposeA48: ( a in D & a <> x & b = xx ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
( ap1 <= xp1 or xp1 <= ap1 ) by A48, A11, DILWORTH:6;
then ( [ap1,x] in the InternalRel of (Mycielskian R) or [x,ap1] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
then ( [an,xx] in the InternalRel of R or [xx,an] in the InternalRel of R ) by A3, A38, A37, Th42, Th43;
hence ( a <= b or b <= a ) by A48, ORDERS_2:def_5; ::_thesis: verum
end;
supposeA49: ( a = xx & b in D & b <> x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
( bp1 <= xp1 or xp1 <= bp1 ) by A49, A11, DILWORTH:6;
then ( [bp1,x] in the InternalRel of (Mycielskian R) or [x,bp1] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
then ( [bn,xx] in the InternalRel of R or [xx,bn] in the InternalRel of R ) by A3, A38, A37, Th42, Th43;
hence ( a <= b or b <= a ) by A49, ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;
then reconsider DD = DD as Clique of R by DILWORTH:6;
A50: not xx in D \ {x} by A40, XBOOLE_0:def_5;
card DD = ((card D) - 1) + 1 by A50, A35, CARD_2:41
.= card D ;
hence contradiction by A9, A7, DILWORTH:def_4; ::_thesis: verum
end;
supposeA51: x = 2 * n ; ::_thesis: contradiction
(2 + 1) - 1 <= (card D) - 1 by A9, A8, XREAL_1:9;
then 2 c= card (D \ {x}) by A35, NAT_1:39;
then consider y, z being set such that
A52: y in D \ {x} and
z in D \ {x} and
y <> z by PENCIL_1:2;
A53: y in D by A52, ZFMISC_1:56;
A54: x <> y by A52, ZFMISC_1:56;
y in the carrier of (Mycielskian R) by A52;
then y in (2 * n) + 1 by Def7;
then reconsider y = y as Nat by NECKLACE:3;
reconsider yp1 = y as Element of (Mycielskian R) by A52;
( yp1 <= xp1 or xp1 <= yp1 ) by A54, A53, A11, DILWORTH:6;
then A55: ( [y,x] in the InternalRel of (Mycielskian R) or [x,y] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5;
y in n by A16, A53, A54;
then A56: y < n by NAT_1:44;
n <= n + n by NAT_1:11;
hence contradiction by A55, A51, A56, Th38; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th47: :: MYCIELSK:47
for R being with_finite_chromatic# RelStr
for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S)
proof
let R be with_finite_chromatic# RelStr ; ::_thesis: for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S)
let S be Subset of R; ::_thesis: chromatic# R >= chromatic# (subrelstr S)
consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
C | S is Coloring of (subrelstr S) by Th10;
then A2: card (C | S) >= chromatic# (subrelstr S) by Def3;
card C >= card (C | S) by Th8;
hence chromatic# R >= chromatic# (subrelstr S) by A1, A2, XXREAL_0:2; ::_thesis: verum
end;
theorem Th48: :: MYCIELSK:48
for n being Nat
for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R)
proof
let n be Nat; ::_thesis: for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R)
let R be irreflexive NatRelStr of n; ::_thesis: chromatic# (Mycielskian R) = 1 + (chromatic# R)
set cR = the carrier of R;
set iR = the InternalRel of R;
set cnR = chromatic# R;
set MR = Mycielskian R;
set cnMR = chromatic# (Mycielskian R);
set cMR = the carrier of (Mycielskian R);
set iMR = the InternalRel of (Mycielskian R);
A1: the carrier of R = n by Def7;
A2: ex C being finite Coloring of (Mycielskian R) st card C = 1 + (chromatic# R)
proof
consider C being finite Coloring of R such that
A3: card C = chromatic# R by Def3;
defpred S1[ set , set ] means $2 = { (m + n) where m is Element of NAT : m in $1 } ;
A4: for e being set st e in C holds
ex u being set st S1[e,u] ;
consider r being Function such that
dom r = C and
A5: for e being set st e in C holds
S1[e,r . e] from CLASSES1:sch_1(A4);
set D = { (d \/ (r . d)) where d is Element of C : d in C } ;
A6: card { (d \/ (r . d)) where d is Element of C : d in C } = card C
proof
percases ( { (d \/ (r . d)) where d is Element of C : d in C } is empty or not { (d \/ (r . d)) where d is Element of C : d in C } is empty ) ;
supposeA7: { (d \/ (r . d)) where d is Element of C : d in C } is empty ; ::_thesis: card { (d \/ (r . d)) where d is Element of C : d in C } = card C
now__::_thesis:_C_is_empty
assume not C is empty ; ::_thesis: contradiction
then consider c being set such that
A8: c in C by XBOOLE_0:def_1;
c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A8;
hence contradiction by A7; ::_thesis: verum
end;
hence card { (d \/ (r . d)) where d is Element of C : d in C } = card C by A7; ::_thesis: verum
end;
supposeA9: not { (d \/ (r . d)) where d is Element of C : d in C } is empty ; ::_thesis: card { (d \/ (r . d)) where d is Element of C : d in C } = card C
defpred S2[ set , set ] means $2 = $1 \/ (r . $1);
A10: for e being set st e in C holds
ex u being set st S2[e,u] ;
consider s being Function such that
A11: dom s = C and
A12: for e being set st e in C holds
S2[e,s . e] from CLASSES1:sch_1(A10);
A13: rng s c= { (d \/ (r . d)) where d is Element of C : d in C }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in { (d \/ (r . d)) where d is Element of C : d in C } )
assume y in rng s ; ::_thesis: y in { (d \/ (r . d)) where d is Element of C : d in C }
then consider x being set such that
A14: x in dom s and
A15: y = s . x by FUNCT_1:def_3;
y = x \/ (r . x) by A14, A15, A11, A12;
hence y in { (d \/ (r . d)) where d is Element of C : d in C } by A14, A11; ::_thesis: verum
end;
then reconsider s = s as Function of C, { (d \/ (r . d)) where d is Element of C : d in C } by A11, FUNCT_2:2;
{ (d \/ (r . d)) where d is Element of C : d in C } c= rng s
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (d \/ (r . d)) where d is Element of C : d in C } or x in rng s )
assume x in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: x in rng s
then consider c being Element of C such that
A16: x = c \/ (r . c) and
A17: c in C ;
x = s . c by A16, A17, A12;
hence x in rng s by A17, A11, FUNCT_1:def_3; ::_thesis: verum
end;
then rng s = { (d \/ (r . d)) where d is Element of C : d in C } by A13, XBOOLE_0:def_10;
then A18: s is onto by FUNCT_2:def_3;
s is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom s or not x2 in dom s or not s . x1 = s . x2 or x1 = x2 )
assume that
A19: x1 in dom s and
A20: x2 in dom s and
A21: s . x1 = s . x2 ; ::_thesis: x1 = x2
A22: s . x1 = x1 \/ (r . x1) by A19, A12;
A23: s . x2 = x2 \/ (r . x2) by A20, A12;
thus x1 c= x2 :: according to XBOOLE_0:def_10 ::_thesis: x2 c= x1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x1 or x in x2 )
assume A24: x in x1 ; ::_thesis: x in x2
A25: x in s . x1 by A22, A24, XBOOLE_0:def_3;
percases ( x in x2 or x in r . x2 ) by A25, A21, A23, XBOOLE_0:def_3;
suppose x in x2 ; ::_thesis: x in x2
hence x in x2 ; ::_thesis: verum
end;
suppose x in r . x2 ; ::_thesis: x in x2
then x in { (m + n) where m is Element of NAT : m in x2 } by A5, A20;
then consider m being Element of NAT such that
A26: x = m + n and
m in x2 ;
m + n < 0 + n by A24, A26, A19, A11, A1, NAT_1:44;
hence x in x2 by XREAL_1:6; ::_thesis: verum
end;
end;
end;
thus x2 c= x1 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x2 or x in x1 )
assume A27: x in x2 ; ::_thesis: x in x1
A28: x in s . x2 by A23, A27, XBOOLE_0:def_3;
percases ( x in x1 or x in r . x1 ) by A28, A21, A22, XBOOLE_0:def_3;
suppose x in x1 ; ::_thesis: x in x1
hence x in x1 ; ::_thesis: verum
end;
suppose x in r . x1 ; ::_thesis: x in x1
then x in { (m + n) where m is Element of NAT : m in x1 } by A5, A19;
then consider m being Element of NAT such that
A29: x = m + n and
m in x1 ;
m + n < 0 + n by A27, A29, A20, A11, A1, NAT_1:44;
hence x in x1 by XREAL_1:6; ::_thesis: verum
end;
end;
end;
end;
hence card { (d \/ (r . d)) where d is Element of C : d in C } = card C by A18, A9, EULER_1:11; ::_thesis: verum
end;
end;
end;
then A30: { (d \/ (r . d)) where d is Element of C : d in C } is finite ;
set E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}};
A31: union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the carrier of (Mycielskian R)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) or x in the carrier of (Mycielskian R) )
assume x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) ; ::_thesis: x in the carrier of (Mycielskian R)
then consider Y being set such that
A32: x in Y and
A33: Y in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by TARSKI:def_4;
percases ( Y in { (d \/ (r . d)) where d is Element of C : d in C } or Y in {{(2 * n)}} ) by A33, XBOOLE_0:def_3;
suppose Y in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: x in the carrier of (Mycielskian R)
then consider d being Element of C such that
A34: Y = d \/ (r . d) and
A35: d in C ;
A36: r . d = { (m + n) where m is Element of NAT : m in d } by A35, A5;
percases ( x in d or x in r . d ) by A32, A34, XBOOLE_0:def_3;
supposeA37: x in d ; ::_thesis: x in the carrier of (Mycielskian R)
reconsider a = x as Nat by A37, A35, A1, NECKLACE:3;
a < n by A37, A35, A1, NAT_1:44;
then a + 0 < n + n by XREAL_1:8;
then a < (2 * n) + 1 by NAT_1:13;
then a in (2 * n) + 1 by NAT_1:44;
hence x in the carrier of (Mycielskian R) by Def7; ::_thesis: verum
end;
suppose x in r . d ; ::_thesis: x in the carrier of (Mycielskian R)
then consider m being Element of NAT such that
A38: x = m + n and
A39: m in d by A36;
m < n by A39, A35, A1, NAT_1:44;
then m + n < n + n by XREAL_1:6;
then m + n < (2 * n) + 1 by NAT_1:13;
then x in (2 * n) + 1 by A38, NAT_1:44;
hence x in the carrier of (Mycielskian R) by Def7; ::_thesis: verum
end;
end;
end;
suppose Y in {{(2 * n)}} ; ::_thesis: x in the carrier of (Mycielskian R)
then Y = {(2 * n)} by TARSKI:def_1;
then A40: x = 2 * n by A32, TARSKI:def_1;
2 * n < (2 * n) + 1 by NAT_1:13;
then 2 * n in (2 * n) + 1 by NAT_1:44;
hence x in the carrier of (Mycielskian R) by A40, Def7; ::_thesis: verum
end;
end;
end;
A41: { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} c= bool the carrier of (Mycielskian R)
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} or X in bool the carrier of (Mycielskian R) )
assume A42: X in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; ::_thesis: X in bool the carrier of (Mycielskian R)
X c= the carrier of (Mycielskian R)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of (Mycielskian R) )
assume x in X ; ::_thesis: x in the carrier of (Mycielskian R)
then x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A42, TARSKI:def_4;
hence x in the carrier of (Mycielskian R) by A31; ::_thesis: verum
end;
hence X in bool the carrier of (Mycielskian R) ; ::_thesis: verum
end;
A43: union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) = the carrier of (Mycielskian R)
proof
thus union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the carrier of (Mycielskian R) by A31; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (Mycielskian R) c= union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}})
thus the carrier of (Mycielskian R) c= union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Mycielskian R) or x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) )
assume x in the carrier of (Mycielskian R) ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}})
then A44: x in (2 * n) + 1 by Def7;
then reconsider a = x as Nat by NECKLACE:3;
a < (2 * n) + 1 by A44, NAT_1:44;
then A45: a <= 2 * n by NAT_1:13;
percases ( a < n or a >= n ) ;
suppose a < n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}})
then a in n by NAT_1:44;
then a in union C by A1, EQREL_1:def_4;
then consider c being set such that
A46: a in c and
A47: c in C by TARSKI:def_4;
A48: x in c \/ (r . c) by A46, XBOOLE_0:def_3;
c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A47;
then c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def_3;
hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A48, TARSKI:def_4; ::_thesis: verum
end;
supposeA49: a >= n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}})
percases ( a < n + n or a = 2 * n ) by A45, XXREAL_0:1;
supposeA50: a < n + n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}})
consider b being Nat such that
A51: a = n + b by A49, NAT_1:10;
reconsider b = b as Element of NAT by ORDINAL1:def_12;
b < n by A51, A50, XREAL_1:6;
then b in the carrier of R by A1, NAT_1:44;
then b in union C by EQREL_1:def_4;
then consider c being set such that
A52: b in c and
A53: c in C by TARSKI:def_4;
r . c = { (m + n) where m is Element of NAT : m in c } by A53, A5;
then a in r . c by A52, A51;
then A54: x in c \/ (r . c) by XBOOLE_0:def_3;
c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A53;
then c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def_3;
hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A54, TARSKI:def_4; ::_thesis: verum
end;
suppose a = 2 * n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}})
then A55: a in {(2 * n)} by TARSKI:def_1;
{(2 * n)} in {{(2 * n)}} by TARSKI:def_1;
then {(2 * n)} in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def_3;
hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A55, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
end;
end;
end;
now__::_thesis:_for_A_being_Subset_of_the_carrier_of_(Mycielskian_R)_st_A_in__{__(d_\/_(r_._d))_where_d_is_Element_of_C_:_d_in_C__}__\/_{{(2_*_n)}}_holds_
(_A_<>_{}_&_(_for_B_being_Subset_of_the_carrier_of_(Mycielskian_R)_st_B_in__{__(d_\/_(r_._d))_where_d_is_Element_of_C_:_d_in_C__}__\/_{{(2_*_n)}}_&_A_<>_B_holds_
not_A_meets_B_)_)
let A be Subset of the carrier of (Mycielskian R); ::_thesis: ( A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} implies ( A <> {} & ( for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds
not A meets B ) ) )
assume A56: A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; ::_thesis: ( A <> {} & ( for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds
not A meets B ) )
thus A <> {} ::_thesis: for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds
not A meets B
proof
percases ( A in { (d \/ (r . d)) where d is Element of C : d in C } or A in {{(2 * n)}} ) by A56, XBOOLE_0:def_3;
suppose A in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: A <> {}
then consider d being Element of C such that
A57: A = d \/ (r . d) and
A58: d in C ;
d <> {} by A58, EQREL_1:def_4;
hence A <> {} by A57; ::_thesis: verum
end;
suppose A in {{(2 * n)}} ; ::_thesis: A <> {}
hence A <> {} by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
let B be Subset of the carrier of (Mycielskian R); ::_thesis: ( B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B implies not A meets B )
assume A59: B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; ::_thesis: ( A <> B implies not A meets B )
assume A60: A <> B ; ::_thesis: not A meets B
assume A meets B ; ::_thesis: contradiction
then consider x being set such that
A61: x in A and
A62: x in B by XBOOLE_0:3;
percases ( ( A in { (d \/ (r . d)) where d is Element of C : d in C } & B in { (d \/ (r . d)) where d is Element of C : d in C } ) or ( A in { (d \/ (r . d)) where d is Element of C : d in C } & B in {{(2 * n)}} ) or ( A in {{(2 * n)}} & B in { (d \/ (r . d)) where d is Element of C : d in C } ) or ( A in {{(2 * n)}} & B in {{(2 * n)}} ) ) by A56, A59, XBOOLE_0:def_3;
supposethat A63: A in { (d \/ (r . d)) where d is Element of C : d in C } and
A64: B in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: contradiction
consider d being Element of C such that
A65: A = d \/ (r . d) and
A66: d in C by A63;
consider e being Element of C such that
A67: B = e \/ (r . e) and
A68: e in C by A64;
percases ( ( x in d & x in e ) or ( x in d & x in r . e ) or ( x in r . d & x in e ) or ( x in r . d & x in r . e ) ) by A65, A67, A61, A62, XBOOLE_0:def_3;
suppose ( x in d & x in e ) ; ::_thesis: contradiction
then d meets e by XBOOLE_0:3;
then d = e by A66, A68, EQREL_1:def_4;
hence contradiction by A65, A67, A60; ::_thesis: verum
end;
supposethat A69: x in d and
A70: x in r . e ; ::_thesis: contradiction
x in { (m + n) where m is Element of NAT : m in e } by A70, A68, A5;
then consider mb being Element of NAT such that
A71: x = mb + n and
mb in e ;
mb + n < n + 0 by A71, A69, A66, A1, NAT_1:44;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
supposethat A72: x in r . d and
A73: x in e ; ::_thesis: contradiction
x in { (m + n) where m is Element of NAT : m in d } by A72, A66, A5;
then consider ma being Element of NAT such that
A74: x = ma + n and
ma in d ;
ma + n < n + 0 by A74, A73, A68, A1, NAT_1:44;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
supposethat A75: x in r . d and
A76: x in r . e ; ::_thesis: contradiction
x in { (m + n) where m is Element of NAT : m in d } by A75, A66, A5;
then consider ma being Element of NAT such that
A77: x = ma + n and
A78: ma in d ;
x in { (m + n) where m is Element of NAT : m in e } by A76, A68, A5;
then consider mb being Element of NAT such that
A79: x = mb + n and
A80: mb in e ;
d meets e by A77, A79, A78, A80, XBOOLE_0:3;
then d = e by A66, A68, EQREL_1:def_4;
hence contradiction by A65, A67, A60; ::_thesis: verum
end;
end;
end;
supposethat A81: A in { (d \/ (r . d)) where d is Element of C : d in C } and
A82: B in {{(2 * n)}} ; ::_thesis: contradiction
B = {(2 * n)} by A82, TARSKI:def_1;
then A83: x = 2 * n by A62, TARSKI:def_1;
consider d being Element of C such that
A84: A = d \/ (r . d) and
A85: d in C by A81;
percases ( x in d or x in r . d ) by A84, A61, XBOOLE_0:def_3;
suppose x in d ; ::_thesis: contradiction
then n + n < n by A85, A1, A83, NAT_1:44;
hence contradiction by NAT_1:11; ::_thesis: verum
end;
suppose x in r . d ; ::_thesis: contradiction
then x in { (m + n) where m is Element of NAT : m in d } by A85, A5;
then consider m being Element of NAT such that
A86: x = m + n and
A87: m in d ;
m in n by A87, A85, A1;
hence contradiction by A86, A83; ::_thesis: verum
end;
end;
end;
supposethat A88: A in {{(2 * n)}} and
A89: B in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: contradiction
A = {(2 * n)} by A88, TARSKI:def_1;
then A90: x = 2 * n by A61, TARSKI:def_1;
consider d being Element of C such that
A91: B = d \/ (r . d) and
A92: d in C by A89;
percases ( x in d or x in r . d ) by A91, A62, XBOOLE_0:def_3;
suppose x in d ; ::_thesis: contradiction
then n + n < n by A92, A1, A90, NAT_1:44;
hence contradiction by NAT_1:11; ::_thesis: verum
end;
suppose x in r . d ; ::_thesis: contradiction
then x in { (m + n) where m is Element of NAT : m in d } by A92, A5;
then consider m being Element of NAT such that
A93: x = m + n and
A94: m in d ;
m in n by A94, A92, A1;
hence contradiction by A93, A90; ::_thesis: verum
end;
end;
end;
suppose ( A in {{(2 * n)}} & B in {{(2 * n)}} ) ; ::_thesis: contradiction
then ( A = {(2 * n)} & B = {(2 * n)} ) by TARSKI:def_1;
hence contradiction by A60; ::_thesis: verum
end;
end;
end;
then reconsider E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} as a_partition of the carrier of (Mycielskian R) by A41, A43, EQREL_1:def_4;
now__::_thesis:_for_x_being_set_st_x_in_E_holds_
x_is_StableSet_of_(Mycielskian_R)
let x be set ; ::_thesis: ( x in E implies b1 is StableSet of (Mycielskian R) )
assume A95: x in E ; ::_thesis: b1 is StableSet of (Mycielskian R)
percases ( x in { (d \/ (r . d)) where d is Element of C : d in C } or x in {{(2 * n)}} ) by A95, XBOOLE_0:def_3;
suppose x in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: b1 is StableSet of (Mycielskian R)
then consider d being Element of C such that
A96: x = d \/ (r . d) and
A97: d in C ;
reconsider d = d as Subset of R by A97;
A98: r . d = { (m + n) where m is Element of NAT : m in d } by A97, A5;
A99: x c= the carrier of (Mycielskian R)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in the carrier of (Mycielskian R) )
assume A100: a in x ; ::_thesis: a in the carrier of (Mycielskian R)
percases ( a in d or a in r . d ) by A96, A100, XBOOLE_0:def_3;
supposeA101: a in d ; ::_thesis: a in the carrier of (Mycielskian R)
then reconsider ap1 = a as Nat by A1, NECKLACE:3;
A102: ap1 < n by A101, A1, NAT_1:44;
n <= n + n by NAT_1:12;
then ap1 < n + n by A102, XXREAL_0:2;
then ap1 < (2 * n) + 1 by NAT_1:13;
then a in (2 * n) + 1 by NAT_1:44;
hence a in the carrier of (Mycielskian R) by Def7; ::_thesis: verum
end;
suppose a in r . d ; ::_thesis: a in the carrier of (Mycielskian R)
then consider am being Element of NAT such that
A103: a = am + n and
A104: am in d by A98;
am < n by A104, A1, NAT_1:44;
then am + n < n + n by XREAL_1:6;
then am + n < (2 * n) + 1 by NAT_1:13;
then a in (2 * n) + 1 by A103, NAT_1:44;
hence a in the carrier of (Mycielskian R) by Def7; ::_thesis: verum
end;
end;
end;
A105: now__::_thesis:_for_x_being_Nat_st_x_in_r_._d_holds_
(_n_<=_x_&_x_<_2_*_n_)
let x be Nat; ::_thesis: ( x in r . d implies ( n <= x & x < 2 * n ) )
assume x in r . d ; ::_thesis: ( n <= x & x < 2 * n )
then consider m being Element of NAT such that
A106: x = m + n and
A107: m in d by A98;
thus n <= x by A106, NAT_1:11; ::_thesis: x < 2 * n
m < n by A107, A1, NAT_1:44;
then m + n < n + n by XREAL_1:6;
hence x < 2 * n by A106; ::_thesis: verum
end;
A108: d is stable by A97, DILWORTH:def_12;
now__::_thesis:_for_a,_b_being_Element_of_(Mycielskian_R)_st_a_in_x_&_b_in_x_&_a_<>_b_holds_
(_not_a_<=_b_&_not_b_<=_a_)
let a, b be Element of (Mycielskian R); ::_thesis: ( a in x & b in x & a <> b implies ( not a <= b & not b <= a ) )
assume that
A109: a in x and
A110: b in x and
A111: a <> b and
A112: ( a <= b or b <= a ) ; ::_thesis: contradiction
A113: ( [a,b] in the InternalRel of (Mycielskian R) or [b,a] in the InternalRel of (Mycielskian R) ) by A112, ORDERS_2:def_5;
percases ( ( a in d & b in d ) or ( a in d & b in r . d ) or ( a in r . d & b in d ) or ( a in r . d & b in r . d ) ) by A109, A110, A96, XBOOLE_0:def_3;
supposeA114: ( a in d & b in d ) ; ::_thesis: contradiction
then A115: ( [a,b] in the InternalRel of R or [b,a] in the InternalRel of R ) by A1, A113, Th40;
reconsider a = a, b = b as Element of R by A114;
( a <= b or b <= a ) by A115, ORDERS_2:def_5;
hence contradiction by A114, A111, A108, DILWORTH:def_2; ::_thesis: verum
end;
supposethat A116: a in d and
A117: b in r . d ; ::_thesis: contradiction
consider bm being Element of NAT such that
A118: b = bm + n and
A119: bm in d by A117, A98;
reconsider ap1 = a as Nat by A116, A1, NECKLACE:3;
A120: ( [ap1,bm] in the InternalRel of R or [bm,ap1] in the InternalRel of R ) by A113, Th42, Th43, A118, A116, A1;
reconsider bmp1 = bm, a = a as Element of R by A119, A116;
A121: ( bmp1 <= a or a <= bmp1 ) by A120, ORDERS_2:def_5;
bmp1 <> a by A120, A116, NECKLACE:def_5;
hence contradiction by A121, A119, A116, A108, DILWORTH:def_2; ::_thesis: verum
end;
supposethat A122: a in r . d and
A123: b in d ; ::_thesis: contradiction
consider am being Element of NAT such that
A124: a = am + n and
A125: am in d by A122, A98;
reconsider bp1 = b as Nat by A123, A1, NECKLACE:3;
A126: ( [am,bp1] in the InternalRel of R or [bp1,am] in the InternalRel of R ) by A113, Th42, Th43, A124, A123, A1;
reconsider amp1 = am, b = b as Element of R by A125, A123;
A127: ( amp1 <= b or b <= amp1 ) by A126, ORDERS_2:def_5;
amp1 <> b by A126, A123, NECKLACE:def_5;
hence contradiction by A127, A125, A123, A108, DILWORTH:def_2; ::_thesis: verum
end;
supposethat A128: a in r . d and
A129: b in r . d ; ::_thesis: contradiction
consider am being Element of NAT such that
A130: a = am + n and
am in d by A128, A98;
consider bm being Element of NAT such that
A131: b = bm + n and
bm in d by A129, A98;
( n <= am + n & am + n < 2 * n & n <= bm + n & bm + n < 2 * n ) by A128, A129, A130, A131, A105;
hence contradiction by A130, A131, A113, Th38; ::_thesis: verum
end;
end;
end;
hence x is StableSet of (Mycielskian R) by A99, DILWORTH:def_2; ::_thesis: verum
end;
suppose x in {{(2 * n)}} ; ::_thesis: b1 is StableSet of (Mycielskian R)
then A132: x = {(2 * n)} by TARSKI:def_1;
2 * n < (2 * n) + 1 by NAT_1:13;
then 2 * n in (2 * n) + 1 by NAT_1:44;
then A133: 2 * n in the carrier of (Mycielskian R) by Def7;
x is Subset of (Mycielskian R) by A132, A133, SUBSET_1:33;
hence x is StableSet of (Mycielskian R) by A132; ::_thesis: verum
end;
end;
end;
then reconsider E = E as Coloring of (Mycielskian R) by DILWORTH:def_12;
take E ; ::_thesis: card E = 1 + (chromatic# R)
now__::_thesis:_not_{(2_*_n)}_in__{__(d_\/_(r_._d))_where_d_is_Element_of_C_:_d_in_C__}_
assume {(2 * n)} in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: contradiction
then consider d being Element of C such that
A134: {(2 * n)} = d \/ (r . d) and
A135: d in C ;
A136: 2 * n in d \/ (r . d) by A134, TARSKI:def_1;
percases ( 2 * n in d or 2 * n in r . d ) by A136, XBOOLE_0:def_3;
suppose 2 * n in d ; ::_thesis: contradiction
then 2 * n in the carrier of R by A135;
then 2 * n in n by Def7;
then n + n < n by NAT_1:44;
hence contradiction by NAT_1:11; ::_thesis: verum
end;
suppose 2 * n in r . d ; ::_thesis: contradiction
then 2 * n in { (m + n) where m is Element of NAT : m in d } by A135, A5;
then consider m being Element of NAT such that
A137: 2 * n = m + n and
A138: m in d ;
m in the carrier of R by A135, A138;
then m in n by Def7;
hence contradiction by A137; ::_thesis: verum
end;
end;
end;
hence card E = 1 + (chromatic# R) by A6, A30, A3, CARD_2:41; ::_thesis: verum
end;
for C being finite Coloring of (Mycielskian R) holds 1 + (chromatic# R) <= card C
proof
let E be finite Coloring of (Mycielskian R); ::_thesis: 1 + (chromatic# R) <= card E
assume 1 + (chromatic# R) > card E ; ::_thesis: contradiction
then A139: chromatic# R >= card E by NAT_1:13;
A140: chromatic# (Mycielskian R) <= card E by Def3;
then A141: chromatic# (Mycielskian R) <= chromatic# R by A139, XXREAL_0:2;
n <= n + n by NAT_1:11;
then n < (2 * n) + 1 by NAT_1:13;
then n c= (2 * n) + 1 by NAT_1:39;
then reconsider S = n as Subset of (Mycielskian R) by Def7;
A142: R = subrelstr S by Th45;
then chromatic# R <= chromatic# (Mycielskian R) by Th47;
then chromatic# R = chromatic# (Mycielskian R) by A141, XXREAL_0:1;
then A143: card E = chromatic# R by A139, A140, XXREAL_0:1;
reconsider C = E | S as Coloring of R by A142, Th10;
A144: card C >= chromatic# R by Def3;
A145: card C <= card E by Th8;
then A146: card C = chromatic# R by A143, A144, XXREAL_0:1;
2 * n < (2 * n) + 1 by NAT_1:13;
then 2 * n in (2 * n) + 1 by NAT_1:44;
then 2 * n in the carrier of (Mycielskian R) by Def7;
then 2 * n in union E by EQREL_1:def_4;
then consider e being set such that
A147: 2 * n in e and
A148: e in E by TARSKI:def_4;
reconsider e = e as Subset of (Mycielskian R) by A148;
reconsider n2 = 2 * n as Element of (Mycielskian R) by A147, A148;
set se = e /\ S;
e meets S by A143, A146, A148, Th9;
then A149: e /\ S in C by A148;
then consider mp1 being Element of R such that
A150: mp1 in e /\ S and
A151: for d being Element of C st d <> e /\ S holds
ex w being Element of R st
( w in Adjacent mp1 & w in d ) by A145, A143, A144, Th31, XXREAL_0:1;
reconsider m = mp1 as Nat by A150, A149, NECKLACE:3;
set mn = m + n;
A152: 0 + n <= m + n by XREAL_1:6;
m < n by A150, A149, NAT_1:44;
then A153: m + n < n + n by XREAL_1:6;
then m + n < (2 * n) + 1 by NAT_1:13;
then A154: m + n in (2 * n) + 1 by NAT_1:44;
then m + n in the carrier of (Mycielskian R) by Def7;
then m + n in union E by EQREL_1:def_4;
then consider f being set such that
A155: m + n in f and
A156: f in E by TARSKI:def_4;
reconsider f = f as Subset of (Mycielskian R) by A156;
reconsider mnp1 = m + n as Element of (Mycielskian R) by A154, Def7;
A157: now__::_thesis:_not_e_<>_f
assume A158: e <> f ; ::_thesis: contradiction
set sf = f /\ S;
f meets S by A143, A146, A156, Th9;
then A159: f /\ S in C by A156;
A160: f /\ S c= f by XBOOLE_1:17;
now__::_thesis:_not_f_/\_S_=_e_/\_S
assume A161: f /\ S = e /\ S ; ::_thesis: contradiction
f /\ S <> {} by A159, EQREL_1:def_4;
then consider x being set such that
A162: x in f /\ S by XBOOLE_0:def_1;
e /\ S c= e by XBOOLE_1:17;
then e meets f by A161, A162, A160, XBOOLE_0:3;
hence contradiction by A158, A156, A148, EQREL_1:def_4; ::_thesis: verum
end;
then consider wp1 being Element of R such that
A163: wp1 in Adjacent mp1 and
A164: wp1 in f /\ S by A159, A151;
reconsider w = wp1 as Nat by A164, A159, NECKLACE:3;
A165: w < n by A164, A159, NAT_1:44;
( mp1 < wp1 or wp1 < mp1 ) by A163, Def6;
then ( mp1 <= wp1 or wp1 <= mp1 ) by ORDERS_2:def_6;
then ( [m,w] in the InternalRel of R or [w,m] in the InternalRel of R ) by ORDERS_2:def_5;
then A166: ( [(m + n),w] in the InternalRel of (Mycielskian R) or [w,(m + n)] in the InternalRel of (Mycielskian R) ) by Th41;
reconsider wp2 = wp1 as Element of (Mycielskian R) by A164;
f is stable by A156, DILWORTH:def_12;
then ( not wp2 <= mnp1 & not mnp1 <= wp2 ) by A165, A152, A164, A160, A155, DILWORTH:def_2;
hence contradiction by A166, ORDERS_2:def_5; ::_thesis: verum
end;
A167: [(m + n),(2 * n)] in the InternalRel of (Mycielskian R) by A153, A152, Th44;
e is stable by A148, DILWORTH:def_12;
then ( not mnp1 <= n2 & not n2 <= mnp1 ) by A147, A155, A157, A153, DILWORTH:def_2;
hence contradiction by A167, ORDERS_2:def_5; ::_thesis: verum
end;
hence chromatic# (Mycielskian R) = 1 + (chromatic# R) by A2, Def3; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_myc1,_myc2_being_Function_st_dom_myc1_=_NAT_&_myc1_._0_=_CompleteRelStr_2_&_(_for_k_being_Nat
for_R_being_NatRelStr_of_(3_*_(2_|^_k))_-'_1_st_R_=_myc1_._k_holds_
myc1_._(k_+_1)_=_Mycielskian_R_)_&_dom_myc2_=_NAT_&_myc2_._0_=_CompleteRelStr_2_&_(_for_k_being_Nat
for_R_being_NatRelStr_of_(3_*_(2_|^_k))_-'_1_st_R_=_myc2_._k_holds_
myc2_._(k_+_1)_=_Mycielskian_R_)_holds_
myc1_=_myc2
let myc1, myc2 be Function; ::_thesis: ( dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds
myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds
myc2 . (k + 1) = Mycielskian R ) implies myc1 = myc2 )
assume that
A1: dom myc1 = NAT and
A2: myc1 . 0 = CompleteRelStr 2 and
A3: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds
myc1 . (k + 1) = Mycielskian R and
A4: dom myc2 = NAT and
A5: myc2 . 0 = CompleteRelStr 2 and
A6: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds
myc2 . (k + 1) = Mycielskian R ; ::_thesis: myc1 = myc2
defpred S1[ Nat] means ( myc1 . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1 & myc1 . $1 = myc2 . $1 );
(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4
.= (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then A7: S1[ 0 ] by A2, A5;
A8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; ::_thesis: S1[k + 1]
reconsider R = myc1 . k as NatRelStr of (3 * (2 |^ k)) -' 1 by A9;
A10: myc1 . (k + 1) = Mycielskian R by A3;
A11: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85;
then 2 |^ k >= 1 by XXREAL_0:2;
then A12: 3 * (2 |^ k) >= 1 by A11, XXREAL_0:2;
then A13: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9;
2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6;
then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64;
then 3 * (2 |^ (k + 1)) >= 1 by A12, XXREAL_0:2;
then A14: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9;
(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A13, XREAL_0:def_2
.= ((3 * (2 * (2 |^ k))) - 2) + 1
.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6
.= (3 * (2 |^ (k + 1))) -' 1 by A14, XREAL_0:def_2 ;
hence S1[k + 1] by A10, A9, A6; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A7, A8);
then for x being set st x in dom myc1 holds
myc1 . x = myc2 . x by A1;
hence myc1 = myc2 by A1, A4, FUNCT_1:2; ::_thesis: verum
end;
definition
let n be Nat;
func Mycielskian n -> NatRelStr of (3 * (2 |^ n)) -' 1 means :Def10: :: MYCIELSK:def 10
ex myc being Function st
( it = 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 ) );
existence
ex b1 being NatRelStr of (3 * (2 |^ n)) -' 1 ex myc being Function st
( b1 = 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 ) )
proof
defpred S1[ Nat, set , set ] means ( ( $2 is NatRelStr of (3 * (2 |^ $1)) -' 1 implies ex R being NatRelStr of (3 * (2 |^ $1)) -' 1 st
( $2 = R & $3 = Mycielskian R ) ) & ( $2 is not NatRelStr of (3 * (2 |^ $1)) -' 1 implies $3 = $2 ) );
A1: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; ::_thesis: ex y being set st S1[n,x,y]
percases ( x is NatRelStr of (3 * (2 |^ n)) -' 1 or not x is NatRelStr of (3 * (2 |^ n)) -' 1 ) ;
suppose x is NatRelStr of (3 * (2 |^ n)) -' 1 ; ::_thesis: ex y being set st S1[n,x,y]
then reconsider R = x as NatRelStr of (3 * (2 |^ n)) -' 1 ;
Mycielskian R = Mycielskian R ;
hence ex y being set st S1[n,x,y] ; ::_thesis: verum
end;
suppose x is not NatRelStr of (3 * (2 |^ n)) -' 1 ; ::_thesis: ex y being set st S1[n,x,y]
hence ex y being set st S1[n,x,y] ; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A2: dom f = NAT and
A3: f . 0 = CompleteRelStr 2 and
A4: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_1(A1);
defpred S2[ Nat] means f . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1;
(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4
.= (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then A5: S2[ 0 ] by A3;
A6: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A7: S2[k] ; ::_thesis: S2[k + 1]
consider R being NatRelStr of (3 * (2 |^ k)) -' 1 such that
f . k = R and
A8: f . (k + 1) = Mycielskian R by A7, A4;
A9: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85;
then 2 |^ k >= 1 by XXREAL_0:2;
then A10: 3 * (2 |^ k) >= 1 by A9, XXREAL_0:2;
then A11: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9;
2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6;
then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64;
then 3 * (2 |^ (k + 1)) >= 1 by A10, XXREAL_0:2;
then A12: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9;
(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A11, XREAL_0:def_2
.= ((3 * (2 * (2 |^ k))) - 2) + 1
.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6
.= (3 * (2 |^ (k + 1))) -' 1 by A12, XREAL_0:def_2 ;
hence S2[k + 1] by A8; ::_thesis: verum
end;
A13: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A5, A6);
n is Element of NAT by ORDINAL1:def_12;
then reconsider IT = f . n as NatRelStr of (3 * (2 |^ n)) -' 1 by A13;
take IT ; ::_thesis: ex myc being Function st
( IT = 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 ) )
take myc = f; ::_thesis: ( IT = 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 ) )
thus IT = myc . n ; ::_thesis: ( 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 ) )
thus dom myc = NAT by A2; ::_thesis: ( 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 ) )
thus myc . 0 = CompleteRelStr 2 by A3; ::_thesis: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R
let k be Nat; ::_thesis: for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R
A14: k is Element of NAT by ORDINAL1:def_12;
let R be NatRelStr of (3 * (2 |^ k)) -' 1; ::_thesis: ( R = myc . k implies myc . (k + 1) = Mycielskian R )
assume A15: R = myc . k ; ::_thesis: myc . (k + 1) = Mycielskian R
then consider RR being NatRelStr of (3 * (2 |^ k)) -' 1 such that
A16: f . k = RR and
A17: f . (k + 1) = Mycielskian RR by A14, A4;
thus myc . (k + 1) = Mycielskian R by A17, A15, A16; ::_thesis: verum
end;
uniqueness
for b1, b2 being NatRelStr of (3 * (2 |^ n)) -' 1 st ex myc being Function st
( b1 = 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 ) ) & 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 ) ) holds
b1 = b2 by Lm1;
end;
:: 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: :: MYCIELSK:49
( Mycielskian 0 = CompleteRelStr 2 & ( for k being Nat holds Mycielskian (k + 1) = Mycielskian (Mycielskian k) ) )
proof
consider myc being Function such that
A1: Mycielskian 0 = myc . 0 and
dom myc = NAT and
A2: myc . 0 = CompleteRelStr 2 and
for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R by Def10;
thus Mycielskian 0 = CompleteRelStr 2 by A1, A2; ::_thesis: for k being Nat holds Mycielskian (k + 1) = Mycielskian (Mycielskian k)
let k be Nat; ::_thesis: Mycielskian (k + 1) = Mycielskian (Mycielskian k)
consider myc1 being Function such that
A3: Mycielskian k = myc1 . k and
A4: ( dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds
myc1 . (k + 1) = Mycielskian R ) ) by Def10;
consider myc2 being Function such that
A5: Mycielskian (k + 1) = myc2 . (k + 1) and
A6: ( dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 ) and
A7: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds
myc2 . (k + 1) = Mycielskian R by Def10;
myc1 = myc2 by A4, A6, A7, Lm1;
hence Mycielskian (k + 1) = Mycielskian (Mycielskian k) by A3, A7, A5; ::_thesis: verum
end;
registration
let n be Nat;
cluster Mycielskian n -> irreflexive ;
coherence
Mycielskian n is irreflexive
proof
defpred S1[ Nat] means Mycielskian n is irreflexive ;
A1: S1[ 0 ] by Th49;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
set cMRn = the carrier of (Mycielskian n);
set iMRn = the InternalRel of (Mycielskian n);
set cMRn1 = the carrier of (Mycielskian (n + 1));
set iMRn1 = the InternalRel of (Mycielskian (n + 1));
assume A3: S1[n] ; ::_thesis: S1[n + 1]
assume not S1[n + 1] ; ::_thesis: contradiction
then consider x being set such that
A4: x in the carrier of (Mycielskian (n + 1)) and
A5: [x,x] in the InternalRel of (Mycielskian (n + 1)) by NECKLACE:def_5;
A6: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Th49;
set N = (3 * (2 |^ n)) -' 1;
A7: the carrier of (Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1 by A6, Def7;
A8: the carrier of (Mycielskian n) = (3 * (2 |^ n)) -' 1 by Def7;
reconsider x = x as Nat by A7, A4, NECKLACE:3;
( ( x < (3 * (2 |^ n)) -' 1 & x < (3 * (2 |^ n)) -' 1 ) or ( x < (3 * (2 |^ n)) -' 1 & (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) & x < (3 * (2 |^ n)) -' 1 ) or ( x = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) & x = 2 * ((3 * (2 |^ n)) -' 1) ) ) by A6, A5, Th38;
then A9: x in (3 * (2 |^ n)) -' 1 by NAT_1:44;
then [x,x] in the InternalRel of (Mycielskian n) by A5, A6, Th40;
hence contradiction by A3, A8, A9, NECKLACE:def_5; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence Mycielskian n is irreflexive ; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster Mycielskian n -> symmetric ;
coherence
Mycielskian n is symmetric
proof
defpred S1[ Nat] means Mycielskian n is symmetric ;
A1: S1[ 0 ] by Th49;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
set cMRn = the carrier of (Mycielskian n);
set iMRn = the InternalRel of (Mycielskian n);
set cMRn1 = the carrier of (Mycielskian (n + 1));
set iMRn1 = the InternalRel of (Mycielskian (n + 1));
assume A3: S1[n] ; ::_thesis: S1[n + 1]
A4: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Th49;
set N = (3 * (2 |^ n)) -' 1;
A5: the carrier of (Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1 by A4, Def7;
A6: the carrier of (Mycielskian n) = (3 * (2 |^ n)) -' 1 by Def7;
let x, y be set ; :: according to RELAT_2:def_3,NECKLACE:def_3 ::_thesis: ( not x in the carrier of (Mycielskian (n + 1)) or not y in the carrier of (Mycielskian (n + 1)) or not [x,y] in the InternalRel of (Mycielskian (n + 1)) or [y,x] in the InternalRel of (Mycielskian (n + 1)) )
assume that
A7: x in the carrier of (Mycielskian (n + 1)) and
A8: y in the carrier of (Mycielskian (n + 1)) and
A9: [x,y] in the InternalRel of (Mycielskian (n + 1)) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))
reconsider xp1 = x, yp1 = y as Nat by A5, A7, A8, NECKLACE:3;
A10: [xp1,yp1] in the InternalRel of (Mycielskian (n + 1)) by A9;
percases ( ( xp1 < (3 * (2 |^ n)) -' 1 & yp1 < (3 * (2 |^ n)) -' 1 ) or ( xp1 < (3 * (2 |^ n)) -' 1 & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 < (3 * (2 |^ n)) -' 1 ) or ( xp1 = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 = 2 * ((3 * (2 |^ n)) -' 1) ) ) by A10, A4, Th38;
suppose ( xp1 < (3 * (2 |^ n)) -' 1 & yp1 < (3 * (2 |^ n)) -' 1 ) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))
then ( xp1 in (3 * (2 |^ n)) -' 1 & yp1 in (3 * (2 |^ n)) -' 1 ) by NAT_1:44;
then A11: [yp1,xp1] in the InternalRel of (Mycielskian n) by A3, A6, Th5, A9, A4, Th40;
the InternalRel of (Mycielskian n) c= the InternalRel of (Mycielskian (n + 1)) by A4, Th39;
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A11; ::_thesis: verum
end;
supposethat A12: xp1 < (3 * (2 |^ n)) -' 1 and
A13: (3 * (2 |^ n)) -' 1 <= yp1 and
A14: yp1 < 2 * ((3 * (2 |^ n)) -' 1) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))
consider yy being Nat such that
A15: yp1 = ((3 * (2 |^ n)) -' 1) + yy by A13, NAT_1:10;
A16: xp1 in (3 * (2 |^ n)) -' 1 by A12, NAT_1:44;
yy + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1) by A14, A15;
then yy < (3 * (2 |^ n)) -' 1 by XREAL_1:6;
then A17: yy in (3 * (2 |^ n)) -' 1 by NAT_1:44;
[x,yy] in the InternalRel of (Mycielskian n) by A9, A16, A15, A4, Th42;
then [yy,x] in the InternalRel of (Mycielskian n) by A17, A16, A6, A3, Th5;
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, A10, A15, Th41; ::_thesis: verum
end;
supposethat A18: (3 * (2 |^ n)) -' 1 <= xp1 and
A19: xp1 < 2 * ((3 * (2 |^ n)) -' 1) and
A20: yp1 < (3 * (2 |^ n)) -' 1 ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))
consider xx being Nat such that
A21: xp1 = ((3 * (2 |^ n)) -' 1) + xx by A18, NAT_1:10;
A22: yp1 in (3 * (2 |^ n)) -' 1 by A20, NAT_1:44;
xx + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1) by A21, A19;
then xx < (3 * (2 |^ n)) -' 1 by XREAL_1:6;
then A23: xx in (3 * (2 |^ n)) -' 1 by NAT_1:44;
[xx,y] in the InternalRel of (Mycielskian n) by A22, A9, A4, A21, Th43;
then [y,xx] in the InternalRel of (Mycielskian n) by A23, A22, A6, A3, Th5;
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, A10, A21, Th41; ::_thesis: verum
end;
suppose ( xp1 = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, Th44; ::_thesis: verum
end;
suppose ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 = 2 * ((3 * (2 |^ n)) -' 1) ) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1))
hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, Th44; ::_thesis: verum
end;
end;
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence Mycielskian n is symmetric ; ::_thesis: verum
end;
end;
theorem Th50: :: MYCIELSK:50
for n being Nat holds
( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) = n + 2 )
proof
defpred S1[ Nat] means ( clique# (Mycielskian $1) = 2 & chromatic# (Mycielskian $1) = $1 + 2 );
A1: clique# (Mycielskian 0) = clique# (CompleteRelStr 2) by Th49
.= 2 by Th33 ;
chromatic# (Mycielskian 0) = chromatic# (CompleteRelStr 2) by Th49
.= 2 by Th35 ;
then A2: S1[ 0 ] by A1;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume that
A4: clique# (Mycielskian n) = 2 and
A5: chromatic# (Mycielskian n) = n + 2 ; ::_thesis: S1[n + 1]
A6: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Th49;
thus clique# (Mycielskian (n + 1)) = 2 by A4, A6, Th46; ::_thesis: chromatic# (Mycielskian (n + 1)) = (n + 1) + 2
thus chromatic# (Mycielskian (n + 1)) = 1 + (chromatic# (Mycielskian n)) by A6, Th48
.= (n + 1) + 2 by A5 ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3);
hence for n being Nat holds
( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) = n + 2 ) ; ::_thesis: verum
end;
theorem :: MYCIELSK:51
for n being Nat ex R being finite RelStr st
( clique# R = 2 & chromatic# R > n )
proof
let n be Nat; ::_thesis: ex R being finite RelStr st
( clique# R = 2 & chromatic# R > n )
take Mycielskian n ; ::_thesis: ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n )
( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13;
then n + 2 > n by XXREAL_0:2;
hence ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n ) by Th50; ::_thesis: verum
end;
theorem :: MYCIELSK:52
for n being Nat ex R being finite RelStr st
( stability# R = 2 & cliquecover# R > n )
proof
let n be Nat; ::_thesis: ex R being finite RelStr st
( stability# R = 2 & cliquecover# R > n )
set R = Mycielskian n;
( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13;
then n + 2 > n by XXREAL_0:2;
then A1: ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n ) by Th50;
take S = ComplRelStr (Mycielskian n); ::_thesis: ( stability# S = 2 & cliquecover# S > n )
thus stability# S = 2 by A1, Th23; ::_thesis: cliquecover# S > n
thus cliquecover# S > n by A1, Th29; ::_thesis: verum
end;