:: DILWORTH semantic presentation
begin
scheme :: DILWORTH:sch 1
FraenkelFinCard1{ F1() -> non empty finite set , P1[ set ], F2() -> finite set , F3( set ) -> set } :
card F2() <= card F1()
provided
A1: F2() = { F3(w) where w is Element of F1() : P1[w] }
proof
A2: F1() is finite ;
set Z = { F3(w) where w is Element of F1() : w in F1() } ;
{ F3(w) where w is Element of F1() : w in F1() } is finite from FRAENKEL:sch_21(A2);
then reconsider Z = { F3(w) where w is Element of F1() : w in F1() } as finite set ;
A3: Z = { F3(w) where w is Element of F1() : w in F1() } ;
A4: card Z <= card F1() from TREES_2:sch_3(A3);
F2() c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F2() or x in Z )
assume x in F2() ; ::_thesis: x in Z
then ex w being Element of F1() st
( x = F3(w) & P1[w] ) by A1;
hence x in Z ; ::_thesis: verum
end;
then card F2() <= card Z by NAT_1:43;
hence card F2() <= card F1() by A4, XXREAL_0:2; ::_thesis: verum
end;
theorem Th1: :: DILWORTH:1
for X, Y, x being set st not x in X holds
X \ (Y \/ {x}) = X \ Y
proof
let X, Y, x be set ; ::_thesis: ( not x in X implies X \ (Y \/ {x}) = X \ Y )
assume not x in X ; ::_thesis: X \ (Y \/ {x}) = X \ Y
then A1: not x in X \ Y ;
thus X \ (Y \/ {x}) = (X \ Y) \ {x} by XBOOLE_1:41
.= X \ Y by A1, ZFMISC_1:57 ; ::_thesis: verum
end;
theorem Th2: :: DILWORTH:2
for X, Y being set
for F being Subset-Family of X
for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)
proof
let X, Y be set ; ::_thesis: for F being Subset-Family of X
for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)
let F be Subset-Family of X; ::_thesis: for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)
let G be Subset-Family of Y; ::_thesis: F \/ G is Subset-Family of (X \/ Y)
A1: F \/ G c= (bool X) \/ (bool Y) by XBOOLE_1:13;
(bool X) \/ (bool Y) c= bool (X \/ Y) by ZFMISC_1:69;
hence F \/ G is Subset-Family of (X \/ Y) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th3: :: DILWORTH:3
for X, Y being set
for F being a_partition of X
for G being a_partition of Y st X misses Y holds
F \/ G is a_partition of X \/ Y
proof
let X, Y be set ; ::_thesis: for F being a_partition of X
for G being a_partition of Y st X misses Y holds
F \/ G is a_partition of X \/ Y
let F be a_partition of X; ::_thesis: for G being a_partition of Y st X misses Y holds
F \/ G is a_partition of X \/ Y
let G be a_partition of Y; ::_thesis: ( X misses Y implies F \/ G is a_partition of X \/ Y )
assume A1: X misses Y ; ::_thesis: F \/ G is a_partition of X \/ Y
set PR = F \/ G;
set XY = X \/ Y;
A2: F \/ G is Subset-Family of (X \/ Y) by Th2;
A3: union (F \/ G) = (union F) \/ (union G) by ZFMISC_1:78
.= X \/ (union G) by EQREL_1:def_4
.= X \/ Y by EQREL_1:def_4 ;
now__::_thesis:_for_A_being_Subset_of_(X_\/_Y)_st_A_in_F_\/_G_holds_
(_A_<>_{}_&_(_for_B_being_Subset_of_(X_\/_Y)_holds_
(_not_B_in_F_\/_G_or_A_=_B_or_A_misses_B_)_)_)
let A be Subset of (X \/ Y); ::_thesis: ( A in F \/ G implies ( A <> {} & ( for B being Subset of (X \/ Y) holds
( not B in F \/ G or b2 = b3 or b2 misses b3 ) ) ) )
assume A4: A in F \/ G ; ::_thesis: ( A <> {} & ( for B being Subset of (X \/ Y) holds
( not B in F \/ G or b2 = b3 or b2 misses b3 ) ) )
( A in F or A in G ) by A4, XBOOLE_0:def_3;
hence A <> {} by EQREL_1:def_4; ::_thesis: for B being Subset of (X \/ Y) holds
( not B in F \/ G or b2 = b3 or b2 misses b3 )
let B be Subset of (X \/ Y); ::_thesis: ( not B in F \/ G or b1 = b2 or b1 misses b2 )
assume A5: B in F \/ G ; ::_thesis: ( b1 = b2 or b1 misses b2 )
percases ( ( A in F & B in F ) or ( A in G & B in G ) or ( A in F & B in G ) or ( A in G & B in F ) ) by A4, A5, XBOOLE_0:def_3;
suppose ( ( A in F & B in F ) or ( A in G & B in G ) ) ; ::_thesis: ( b1 = b2 or b1 misses b2 )
hence ( A = B or A misses B ) by EQREL_1:def_4; ::_thesis: verum
end;
suppose ( ( A in F & B in G ) or ( A in G & B in F ) ) ; ::_thesis: ( b1 = b2 or b1 misses b2 )
hence ( A = B or A misses B ) by A1, XBOOLE_1:64; ::_thesis: verum
end;
end;
end;
hence F \/ G is a_partition of X \/ Y by A2, A3, EQREL_1:def_4; ::_thesis: verum
end;
theorem Th4: :: DILWORTH:4
for X, Y being set
for F being a_partition of Y st Y c< X holds
F \/ {(X \ Y)} is a_partition of X
proof
let X, Y be set ; ::_thesis: for F being a_partition of Y st Y c< X holds
F \/ {(X \ Y)} is a_partition of X
let F be a_partition of Y; ::_thesis: ( Y c< X implies F \/ {(X \ Y)} is a_partition of X )
assume A1: Y c< X ; ::_thesis: F \/ {(X \ Y)} is a_partition of X
then A2: X \ Y <> {} by XBOOLE_1:105;
Y c= X by A1, XBOOLE_0:def_8;
then A3: Y \/ (X \ Y) = X by XBOOLE_1:45;
{(X \ Y)} is a_partition of X \ Y by A2, EQREL_1:39;
hence F \/ {(X \ Y)} is a_partition of X by A3, Th3, XBOOLE_1:79; ::_thesis: verum
end;
theorem Th5: :: DILWORTH:5
for X being infinite set
for n being Nat ex Y being finite Subset of X st card Y > n
proof
let X be infinite set ; ::_thesis: for n being Nat ex Y being finite Subset of X st card Y > n
let n be Nat; ::_thesis: ex Y being finite Subset of X st card Y > n
consider f being Function of NAT,X such that
A1: f is one-to-one by DICKSON:3;
set Sn = Seg (n + 1);
reconsider ff = f | (Seg (n + 1)) as Function of (Seg (n + 1)),X by FUNCT_2:32;
ff is one-to-one by A1, FUNCT_1:52;
then card ff = card (rng ff) by PRE_POLY:19;
then A2: card (dom ff) = card (rng ff) by CARD_1:62;
reconsider Y = rng ff as finite Subset of X by RELAT_1:def_19;
take Y ; ::_thesis: card Y > n
dom ff = Seg (n + 1) by FUNCT_2:def_1;
then card (dom ff) = n + 1 by FINSEQ_1:57;
hence card Y > n by A2, NAT_1:13; ::_thesis: verum
end;
begin
definition
let R be RelStr ;
let S be Subset of R;
attrS is connected means :Def1: :: DILWORTH:def 1
the InternalRel of R is_connected_in S;
end;
:: deftheorem Def1 defines connected DILWORTH:def_1_:_
for R being RelStr
for S being Subset of R holds
( S is connected iff the InternalRel of R is_connected_in S );
notation
let R be RelStr ;
let S be Subset of R;
synonym clique S for connected ;
end;
registration
let R be RelStr ;
cluster trivial -> clique for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is trivial holds
b1 is clique
proof
let S be Subset of R; ::_thesis: ( S is trivial implies S is clique )
assume A1: S is trivial ; ::_thesis: S is clique
let x1, x2 be set ; :: according to RELAT_2:def_6,DILWORTH:def_1 ::_thesis: ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
thus ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
end;
registration
let R be RelStr ;
cluster clique for Element of bool the carrier of R;
existence
ex b1 being Subset of R st b1 is clique
proof
take {} R ; ::_thesis: {} R is clique
let x1, x2 be set ; :: according to RELAT_2:def_6,DILWORTH:def_1 ::_thesis: ( not x1 in {} R or not x2 in {} R or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
thus ( not x1 in {} R or not x2 in {} R or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) ; ::_thesis: verum
end;
end;
definition
let R be RelStr ;
mode Clique of R is clique Subset of R;
end;
theorem Th6: :: DILWORTH:6
for R being RelStr
for S being Subset of R holds
( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a )
proof
let R be RelStr ; ::_thesis: for S being Subset of R holds
( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a )
let S be Subset of R; ::_thesis: ( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a )
set RR = the InternalRel of R;
hereby ::_thesis: ( ( for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a ) implies S is Clique of R )
assume S is Clique of R ; ::_thesis: for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a
then A1: the InternalRel of R is_connected_in S by Def1;
let a, b be Element of R; ::_thesis: ( a in S & b in S & a <> b & not a <= b implies b <= a )
assume ( a in S & b in S & a <> b ) ; ::_thesis: ( a <= b or b <= a )
then ( [a,b] in the InternalRel of R or [b,a] in the InternalRel of R ) by A1, RELAT_2:def_6;
hence ( a <= b or b <= a ) by ORDERS_2:def_5; ::_thesis: verum
end;
assume A2: for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a ; ::_thesis: S is Clique of R
the InternalRel of R is_connected_in S
proof
let x, y be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x in S or not y in S or x = y or [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
assume A3: ( x in S & y in S & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
then reconsider x9 = x, y9 = y as Element of R ;
( x9 <= y9 or y9 <= x9 ) by A3, A2;
hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by ORDERS_2:def_5; ::_thesis: verum
end;
hence S is Clique of R by Def1; ::_thesis: verum
end;
registration
let R be RelStr ;
cluster finite connected for Element of bool the carrier of R;
existence
ex b1 being Clique of R st b1 is finite
proof
take {} R ; ::_thesis: {} R is finite
thus {} R is finite ; ::_thesis: verum
end;
end;
registration
let R be reflexive RelStr ;
cluster connected -> strongly_connected for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is connected holds
b1 is strongly_connected
proof
let C be Subset of R; ::_thesis: ( C is connected implies C is strongly_connected )
set iR = the InternalRel of R;
set cR = the carrier of R;
assume C is clique ; ::_thesis: C is strongly_connected
then A1: the InternalRel of R is_connected_in C by Def1;
A2: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def_2;
thus C is strongly_connected ::_thesis: verum
proof
let x, y be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: ( not x in C or not y in C or [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
assume that
A3: x in C and
A4: y in C ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by A3, A2, RELAT_2:def_1; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by A3, A4, A1, RELAT_2:def_6; ::_thesis: verum
end;
end;
end;
end;
end;
registration
let R be non empty RelStr ;
cluster non empty finite connected for Element of bool the carrier of R;
existence
ex b1 being Clique of R st
( b1 is finite & not b1 is empty )
proof
{ the Element of R} is clique ;
hence ex b1 being Clique of R st
( b1 is finite & not b1 is empty ) ; ::_thesis: verum
end;
end;
theorem :: DILWORTH:7
for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds
a2 <= a1
proof
let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds
a2 <= a1
let a1, a2 be Element of R; ::_thesis: ( a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 implies a2 <= a1 )
assume A1: a1 <> a2 ; ::_thesis: ( not {a1,a2} is Clique of R or a1 <= a2 or a2 <= a1 )
A2: ( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def_2;
assume {a1,a2} is Clique of R ; ::_thesis: ( a1 <= a2 or a2 <= a1 )
hence ( a1 <= a2 or a2 <= a1 ) by A2, A1, Th6; ::_thesis: verum
end;
theorem Th8: :: DILWORTH:8
for R being non empty RelStr
for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds
{a1,a2} is Clique of R
proof
let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds
{a1,a2} is Clique of R
let a1, a2 be Element of R; ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Clique of R )
assume A1: ( a1 <= a2 or a2 <= a1 ) ; ::_thesis: {a1,a2} is Clique of R
now__::_thesis:_for_x,_y_being_Element_of_R_st_x_in_{a1,a2}_&_y_in_{a1,a2}_&_x_<>_y_&_not_x_<=_y_holds_
y_<=_x
let x, y be Element of R; ::_thesis: ( x in {a1,a2} & y in {a1,a2} & x <> y & not x <= y implies y <= x )
assume ( x in {a1,a2} & y in {a1,a2} ) ; ::_thesis: ( not x <> y or x <= y or y <= x )
then A2: ( ( x = a1 or x = a2 ) & ( y = a1 or y = a2 ) ) by TARSKI:def_2;
assume x <> y ; ::_thesis: ( x <= y or y <= x )
hence ( x <= y or y <= x ) by A1, A2; ::_thesis: verum
end;
hence {a1,a2} is Clique of R by Th6; ::_thesis: verum
end;
theorem Th9: :: DILWORTH:9
for R being RelStr
for C being Clique of R
for S being Subset of C holds S is Clique of R
proof
let R be RelStr ; ::_thesis: for C being Clique of R
for S being Subset of C holds S is Clique of R
let C be Clique of R; ::_thesis: for S being Subset of C holds S is Clique of R
let S be Subset of C; ::_thesis: S is Clique of R
set iR = the InternalRel of R;
A1: the InternalRel of R is_connected_in C by Def1;
the InternalRel of R is_connected_in S
proof
let x1, x2 be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
assume ( x1 in S & x2 in S & x1 <> x2 ) ; ::_thesis: ( [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
hence ( [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) by A1, RELAT_2:def_6; ::_thesis: verum
end;
hence S is Clique of R by Def1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: DILWORTH:10
for R being RelStr
for C being finite Clique of R
for n being Nat st n <= card C holds
ex B being finite Clique of R st
( B c= C & card B = n )
proof
let R be RelStr ; ::_thesis: for C being finite Clique of R
for n being Nat st n <= card C holds
ex B being finite Clique of R st
( B c= C & card B = n )
let C be finite Clique of R; ::_thesis: for n being Nat st n <= card C holds
ex B being finite Clique of R st
( B c= C & card B = n )
let n be Nat; ::_thesis: ( n <= card C implies ex B being finite Clique of R st
( B c= C & card B = n ) )
assume A1: n <= card C ; ::_thesis: ex B being finite Clique of R st
( B c= C & card B = n )
consider BB being finite Subset of C such that
A2: card BB = n by A1, FINSEQ_4:72;
reconsider BB = BB as finite Clique of R by Th9;
take BB ; ::_thesis: ( BB c= C & card BB = n )
thus ( BB c= C & card BB = n ) by A2; ::_thesis: verum
end;
theorem Th11: :: DILWORTH:11
for R being transitive RelStr
for C being Clique of R
for x, y being Element of R st x is_maximal_in C & x <= y holds
C \/ {y} is Clique of R
proof
let R be transitive RelStr ; ::_thesis: for C being Clique of R
for x, y being Element of R st x is_maximal_in C & x <= y holds
C \/ {y} is Clique of R
let C be Clique of R; ::_thesis: for x, y being Element of R st x is_maximal_in C & x <= y holds
C \/ {y} is Clique of R
let x, y be Element of R; ::_thesis: ( x is_maximal_in C & x <= y implies C \/ {y} is Clique of R )
assume that
A1: x is_maximal_in C and
A2: x <= y ; ::_thesis: C \/ {y} is Clique of R
A3: x in C by A1, WAYBEL_4:55;
A4: not the carrier of R is empty by A1, WAYBEL_4:55;
set Cb = C \/ {y};
A5: C \/ {y} c= the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C \/ {y} or x in the carrier of R )
assume A6: x in C \/ {y} ; ::_thesis: x in the carrier of R
percases ( x in C or x in {y} ) by A6, XBOOLE_0:def_3;
suppose x in C ; ::_thesis: x in the carrier of R
hence x in the carrier of R ; ::_thesis: verum
end;
suppose x in {y} ; ::_thesis: x in the carrier of R
then x = y by TARSKI:def_1;
hence x in the carrier of R by A4; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_C_\/_{y}_&_b_in_C_\/_{y}_&_a_<>_b_&_not_a_<=_b_holds_
b_<=_a
let a, b be Element of R; ::_thesis: ( a in C \/ {y} & b in C \/ {y} & a <> b & not b1 <= b2 implies b2 <= b1 )
assume that
A7: ( a in C \/ {y} & b in C \/ {y} ) and
A8: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
percases ( ( a in C & b in C ) or ( a in C & b in {y} ) or ( a in {y} & b in C ) or ( a in {y} & b in {y} ) ) by A7, XBOOLE_0:def_3;
suppose ( a in C & b in C ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A8, Th6; ::_thesis: verum
end;
supposethat A9: a in C and
A10: b in {y} ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
A11: b = y by A10, TARSKI:def_1;
A12: not x < a by A1, A9, WAYBEL_4:55;
percases ( x <> a or x = a ) ;
suppose x <> a ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then ( a <= x or x <= a ) by A9, A3, Th6;
hence ( a <= b or b <= a ) by A2, A11, A12, ORDERS_2:3, ORDERS_2:def_6; ::_thesis: verum
end;
suppose x = a ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A2, A10, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
supposethat A13: a in {y} and
A14: b in C ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
A15: a = y by A13, TARSKI:def_1;
A16: not x < b by A1, A14, WAYBEL_4:55;
percases ( x <> b or x = b ) ;
suppose x <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then ( b <= x or x <= b ) by A14, A3, Th6;
hence ( a <= b or b <= a ) by A2, A15, A16, ORDERS_2:3, ORDERS_2:def_6; ::_thesis: verum
end;
suppose x = b ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A2, A13, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
suppose ( a in {y} & b in {y} ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then ( a = y & b = y ) by TARSKI:def_1;
hence ( a <= b or b <= a ) by A8; ::_thesis: verum
end;
end;
end;
hence C \/ {y} is Clique of R by A5, Th6; ::_thesis: verum
end;
theorem Th12: :: DILWORTH:12
for R being transitive RelStr
for C being Clique of R
for x, y being Element of R st x is_minimal_in C & y <= x holds
C \/ {y} is Clique of R
proof
let R be transitive RelStr ; ::_thesis: for C being Clique of R
for x, y being Element of R st x is_minimal_in C & y <= x holds
C \/ {y} is Clique of R
let C be Clique of R; ::_thesis: for x, y being Element of R st x is_minimal_in C & y <= x holds
C \/ {y} is Clique of R
let x, y be Element of R; ::_thesis: ( x is_minimal_in C & y <= x implies C \/ {y} is Clique of R )
assume that
A1: x is_minimal_in C and
A2: y <= x ; ::_thesis: C \/ {y} is Clique of R
A3: x in C by A1, WAYBEL_4:56;
A4: not the carrier of R is empty by A1, WAYBEL_4:56;
set Cb = C \/ {y};
A5: C \/ {y} c= the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C \/ {y} or x in the carrier of R )
assume A6: x in C \/ {y} ; ::_thesis: x in the carrier of R
percases ( x in C or x in {y} ) by A6, XBOOLE_0:def_3;
suppose x in C ; ::_thesis: x in the carrier of R
hence x in the carrier of R ; ::_thesis: verum
end;
suppose x in {y} ; ::_thesis: x in the carrier of R
then x = y by TARSKI:def_1;
hence x in the carrier of R by A4; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_C_\/_{y}_&_b_in_C_\/_{y}_&_a_<>_b_&_not_a_<=_b_holds_
b_<=_a
let a, b be Element of R; ::_thesis: ( a in C \/ {y} & b in C \/ {y} & a <> b & not b1 <= b2 implies b2 <= b1 )
assume that
A7: ( a in C \/ {y} & b in C \/ {y} ) and
A8: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
percases ( ( a in C & b in C ) or ( a in C & b in {y} ) or ( a in {y} & b in C ) or ( a in {y} & b in {y} ) ) by A7, XBOOLE_0:def_3;
suppose ( a in C & b in C ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A8, Th6; ::_thesis: verum
end;
supposethat A9: a in C and
A10: b in {y} ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
A11: b = y by A10, TARSKI:def_1;
A12: not a < x by A1, A9, WAYBEL_4:56;
percases ( a <> x or x = a ) ;
supposeA13: a <> x ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then not a <= x by A12, ORDERS_2:def_6;
then x <= a by A9, A3, A13, Th6;
hence ( a <= b or b <= a ) by A2, A11, ORDERS_2:3; ::_thesis: verum
end;
suppose x = a ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A2, A10, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
supposethat A14: a in {y} and
A15: b in C ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
A16: a = y by A14, TARSKI:def_1;
A17: not b < x by A1, A15, WAYBEL_4:56;
percases ( b <> x or x = b ) ;
supposeA18: b <> x ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then not b <= x by A17, ORDERS_2:def_6;
then x <= b by A15, A3, A18, Th6;
hence ( a <= b or b <= a ) by A2, A16, ORDERS_2:3; ::_thesis: verum
end;
suppose x = b ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A2, A14, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
suppose ( a in {y} & b in {y} ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then ( a = y & b = y ) by TARSKI:def_1;
hence ( a <= b or b <= a ) by A8; ::_thesis: verum
end;
end;
end;
hence C \/ {y} is Clique of R by A5, Th6; ::_thesis: verum
end;
definition
let R be RelStr ;
let S be Subset of R;
attrS is stable means :Def2: :: DILWORTH:def 2
for x, y being Element of R st x in S & y in S & x <> y holds
( not x <= y & not y <= x );
end;
:: deftheorem Def2 defines stable DILWORTH:def_2_:_
for R being RelStr
for S being Subset of R holds
( S is stable iff for x, y being Element of R st x in S & y in S & x <> y holds
( not x <= y & not y <= x ) );
registration
let R be RelStr ;
cluster trivial -> stable for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is trivial holds
b1 is stable
proof
let S be Subset of R; ::_thesis: ( S is trivial implies S is stable )
assume A1: S is trivial ; ::_thesis: S is stable
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) )
thus ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) ) by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
end;
registration
let R be RelStr ;
cluster stable for Element of bool the carrier of R;
existence
ex b1 being Subset of R st b1 is stable
proof
reconsider A = {} as Subset of R by XBOOLE_1:2;
take A ; ::_thesis: A is stable
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in A & y in A & x <> y implies ( not x <= y & not y <= x ) )
thus ( x in A & y in A & x <> y implies ( not x <= y & not y <= x ) ) ; ::_thesis: verum
end;
end;
definition
let R be RelStr ;
mode StableSet of R is stable Subset of R;
end;
registration
let R be RelStr ;
cluster finite stable for Element of bool the carrier of R;
existence
ex b1 being StableSet of R st b1 is finite
proof
take {} R ; ::_thesis: {} R is finite
thus {} R is finite ; ::_thesis: verum
end;
end;
registration
let R be non empty RelStr ;
cluster non empty finite stable for Element of bool the carrier of R;
existence
ex b1 being StableSet of R st
( b1 is finite & not b1 is empty )
proof
{ the Element of R} is stable ;
hence ex b1 being StableSet of R st
( b1 is finite & not b1 is empty ) ; ::_thesis: verum
end;
end;
theorem :: DILWORTH:13
for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds
( not a1 <= a2 & not a2 <= a1 )
proof
let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds
( not a1 <= a2 & not a2 <= a1 )
let a1, a2 be Element of R; ::_thesis: ( a1 <> a2 & {a1,a2} is StableSet of R implies ( not a1 <= a2 & not a2 <= a1 ) )
assume A1: a1 <> a2 ; ::_thesis: ( not {a1,a2} is StableSet of R or ( not a1 <= a2 & not a2 <= a1 ) )
A2: ( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def_2;
assume {a1,a2} is StableSet of R ; ::_thesis: ( not a1 <= a2 & not a2 <= a1 )
hence ( not a1 <= a2 & not a2 <= a1 ) by A2, A1, Def2; ::_thesis: verum
end;
theorem Th14: :: DILWORTH:14
for R being non empty RelStr
for a1, a2 being Element of R holds
( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )
proof
let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R holds
( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )
let a1, a2 be Element of R; ::_thesis: ( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )
assume A1: ( not a1 <= a2 & not a2 <= a1 ) ; ::_thesis: {a1,a2} is StableSet of R
set S = {a1,a2};
{a1,a2} is stable
proof
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in {a1,a2} & y in {a1,a2} & x <> y implies ( not x <= y & not y <= x ) )
assume A2: ( x in {a1,a2} & y in {a1,a2} & x <> y ) ; ::_thesis: ( not x <= y & not y <= x )
( ( x = a1 or x = a2 ) & ( y = a1 or y = a2 ) ) by A2, TARSKI:def_2;
hence ( not x <= y & not y <= x ) by A1, A2; ::_thesis: verum
end;
hence {a1,a2} is StableSet of R ; ::_thesis: verum
end;
theorem Th15: :: DILWORTH:15
for R being RelStr
for C being Clique of R
for A being StableSet of R
for a, b being set st a in A & b in A & a in C & b in C holds
a = b
proof
let R be RelStr ; ::_thesis: for C being Clique of R
for A being StableSet of R
for a, b being set st a in A & b in A & a in C & b in C holds
a = b
let C be Clique of R; ::_thesis: for A being StableSet of R
for a, b being set st a in A & b in A & a in C & b in C holds
a = b
let A be StableSet of R; ::_thesis: for a, b being set st a in A & b in A & a in C & b in C holds
a = b
let a, b be set ; ::_thesis: ( a in A & b in A & a in C & b in C implies a = b )
assume that
A1: ( a in A & b in A ) and
A2: ( a in C & b in C ) ; ::_thesis: a = b
assume A3: a <> b ; ::_thesis: contradiction
reconsider a9 = a, b9 = b as Element of R by A1;
( not a9 <= b9 & not b9 <= a9 ) by A1, A3, Def2;
hence contradiction by A2, A3, Th6; ::_thesis: verum
end;
theorem Th16: :: DILWORTH:16
for R being RelStr
for A being StableSet of R
for B being Subset of A holds B is StableSet of R
proof
let R be RelStr ; ::_thesis: for A being StableSet of R
for B being Subset of A holds B is StableSet of R
let A be StableSet of R; ::_thesis: for B being Subset of A holds B is StableSet of R
let B be Subset of A; ::_thesis: B is StableSet of R
reconsider BB = B as Subset of R by XBOOLE_1:1;
BB is stable
proof
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in BB & y in BB & x <> y implies ( not x <= y & not y <= x ) )
assume A1: ( x in BB & y in BB & x <> y ) ; ::_thesis: ( not x <= y & not y <= x )
thus ( not x <= y & not y <= x ) by A1, Def2; ::_thesis: verum
end;
hence B is StableSet of R ; ::_thesis: verum
end;
theorem Th17: :: DILWORTH:17
for R being RelStr
for A being finite StableSet of R
for n being Nat st n <= card A holds
ex B being finite StableSet of R st card B = n
proof
let R be RelStr ; ::_thesis: for A being finite StableSet of R
for n being Nat st n <= card A holds
ex B being finite StableSet of R st card B = n
let A be finite StableSet of R; ::_thesis: for n being Nat st n <= card A holds
ex B being finite StableSet of R st card B = n
let n be Nat; ::_thesis: ( n <= card A implies ex B being finite StableSet of R st card B = n )
assume A1: n <= card A ; ::_thesis: ex B being finite StableSet of R st card B = n
consider BB being finite Subset of A such that
A2: card BB = n by A1, FINSEQ_4:72;
reconsider BB = BB as finite StableSet of R by Th16;
take BB ; ::_thesis: card BB = n
thus card BB = n by A2; ::_thesis: verum
end;
begin
definition
let R be RelStr ;
attrR is with_finite_clique# means :Def3: :: DILWORTH:def 3
ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C;
end;
:: deftheorem Def3 defines with_finite_clique# DILWORTH:def_3_:_
for R being RelStr holds
( R is with_finite_clique# iff ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C );
registration
cluster finite -> with_finite_clique# for RelStr ;
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_clique#
proof
let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_clique# )
assume R is finite ; ::_thesis: R is with_finite_clique#
then reconsider R9 = R as finite RelStr ;
defpred S1[ Nat] means ex c being finite Clique of R st card c = c1;
A1: for k being Nat st S1[k] holds
k <= card R9 by NAT_1:43;
card ({} R) = 0 ;
then A2: ex k being Nat st S1[k] ;
consider k being Nat such that
A3: S1[k] and
A4: for n being Nat st S1[n] holds
n <= k from NAT_1:sch_6(A1, A2);
consider c being finite Clique of R such that
A5: card c = k by A3;
for D being finite Clique of R holds card D <= card c by A5, A4;
hence R is with_finite_clique# by Def3; ::_thesis: verum
end;
end;
registration
let R be with_finite_clique# RelStr ;
cluster connected -> finite for Element of bool the carrier of R;
coherence
for b1 being Clique of R holds b1 is finite
proof
let D be Clique of R; ::_thesis: D is finite
consider C being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card C by Def3;
assume D is infinite ; ::_thesis: contradiction
then consider Y being finite Subset of D such that
A2: card Y > card C by Th5;
Y is Clique of R by Th9;
hence contradiction by A2, A1; ::_thesis: verum
end;
end;
definition
let R be with_finite_clique# RelStr ;
func clique# R -> Nat means :Def4: :: DILWORTH:def 4
( ex C being finite Clique of R st card C = it & ( for T being finite Clique of R holds card T <= it ) );
existence
ex b1 being Nat st
( ex C being finite Clique of R st card C = b1 & ( for T being finite Clique of R holds card T <= b1 ) )
proof
consider A being finite Clique of R such that
A1: for B being finite Clique of R holds card B <= card A by Def3;
take itt = card A; ::_thesis: ( ex C being finite Clique of R st card C = itt & ( for T being finite Clique of R holds card T <= itt ) )
thus ex A being finite Clique of R st card A = itt ; ::_thesis: for T being finite Clique of R holds card T <= itt
let T be finite Clique of R; ::_thesis: card T <= itt
thus card T <= itt by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Nat st ex C being finite Clique of R st card C = b1 & ( for T being finite Clique of R holds card T <= b1 ) & ex C being finite Clique of R st card C = b2 & ( for T being finite Clique of R holds card T <= b2 ) holds
b1 = b2
proof
let it1, it2 be Nat; ::_thesis: ( ex C being finite Clique of R st card C = it1 & ( for T being finite Clique of R holds card T <= it1 ) & ex C being finite Clique of R st card C = it2 & ( for T being finite Clique of R holds card T <= it2 ) implies it1 = it2 )
assume that
A2: ex S1 being finite Clique of R st card S1 = it1 and
A3: for T being finite Clique of R holds card T <= it1 and
A4: ex S2 being finite Clique of R st card S2 = it2 and
A5: for T being finite Clique of R holds card T <= it2 ; ::_thesis: it1 = it2
consider S1 being finite Clique of R such that
A6: card S1 = it1 by A2;
consider S2 being finite Clique of R such that
A7: card S2 = it2 by A4;
( it1 <= it2 & it2 <= it1 ) by A6, A7, A3, A5;
hence it1 = it2 by XXREAL_0:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines clique# DILWORTH:def_4_:_
for R being with_finite_clique# RelStr
for b2 being Nat holds
( b2 = clique# R iff ( ex C being finite Clique of R st card C = b2 & ( for T being finite Clique of R holds card T <= b2 ) ) );
registration
let R be empty RelStr ;
cluster clique# R -> empty ;
coherence
clique# R is empty
proof
for T being Clique of R holds card T <= card ({} R) ;
hence clique# R is empty by Def4; ::_thesis: verum
end;
end;
registration
let R be non empty with_finite_clique# RelStr ;
cluster clique# R -> positive ;
coherence
clique# R is positive
proof
card { the Element of R} <= clique# R by Def4;
hence clique# R is positive ; ::_thesis: verum
end;
end;
theorem :: DILWORTH:18
for R being non empty with_finite_clique# RelStr st [#] R is StableSet of R holds
clique# R = 1
proof
let R be non empty with_finite_clique# RelStr ; ::_thesis: ( [#] R is StableSet of R implies clique# R = 1 )
assume A1: [#] R is StableSet of R ; ::_thesis: clique# R = 1
A2: clique# R >= 0 + 1 by NAT_1:13;
consider A being finite Clique of R such that
A3: card A = clique# R by Def4;
assume clique# R <> 1 ; ::_thesis: contradiction
then card A > 1 by A2, A3, XXREAL_0:1;
then consider a, b being set such that
A4: a in A and
A5: b in A and
A6: a <> b by NAT_1:59;
thus contradiction by A4, A5, A6, A1, Th15; ::_thesis: verum
end;
theorem Th19: :: DILWORTH:19
for R being with_finite_clique# RelStr st clique# R = 1 holds
[#] R is StableSet of R
proof
let R be with_finite_clique# RelStr ; ::_thesis: ( clique# R = 1 implies [#] R is StableSet of R )
assume A1: clique# R = 1 ; ::_thesis: [#] R is StableSet of R
set cR = the carrier of R;
A2: not R is empty by A1;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_the_carrier_of_R_&_b_in_the_carrier_of_R_&_a_<>_b_holds_
(_not_a_<=_b_&_not_b_<=_a_)
let a, b be Element of R; ::_thesis: ( a in the carrier of R & b in the carrier of R & a <> b implies ( not a <= b & not b <= a ) )
assume that
a in the carrier of R and
b in the carrier of R and
A3: a <> b ; ::_thesis: ( not a <= b & not b <= a )
assume ( a <= b or b <= a ) ; ::_thesis: contradiction
then A4: {a,b} is Clique of R by A2, Th8;
card {a,b} = 2 by A3, CARD_2:57;
hence contradiction by A4, A1, Def4; ::_thesis: verum
end;
hence [#] R is StableSet of R by Def2; ::_thesis: verum
end;
definition
let R be RelStr ;
attrR is with_finite_stability# means :Def5: :: DILWORTH:def 5
ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A;
end;
:: deftheorem Def5 defines with_finite_stability# DILWORTH:def_5_:_
for R being RelStr holds
( R is with_finite_stability# iff ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A );
registration
cluster finite -> with_finite_stability# for RelStr ;
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_stability#
proof
let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_stability# )
assume R is finite ; ::_thesis: R is with_finite_stability#
then reconsider R9 = R as finite RelStr ;
defpred S1[ Nat] means ex A being finite StableSet of R9 st card A = c1;
A1: for k being Nat st S1[k] holds
k <= card R9 by NAT_1:43;
( {} R is StableSet of R & card {} = 0 ) ;
then A2: ex k being Nat st S1[k] ;
consider k being Nat such that
A3: S1[k] and
A4: for n being Nat st S1[n] holds
n <= k from NAT_1:sch_6(A1, A2);
consider S being finite StableSet of R such that
A5: card S = k by A3;
take S ; :: according to DILWORTH:def_5 ::_thesis: for B being finite StableSet of R holds card B <= card S
let T be finite StableSet of R; ::_thesis: card T <= card S
thus card T <= card S by A5, A4; ::_thesis: verum
end;
end;
registration
let R be with_finite_stability# RelStr ;
cluster stable -> finite for Element of bool the carrier of R;
coherence
for b1 being StableSet of R holds b1 is finite
proof
consider A being finite StableSet of R such that
A1: for B being finite StableSet of R holds card A >= card B by Def5;
given B being StableSet of R such that A2: B is infinite ; ::_thesis: contradiction
consider C being finite Subset of B such that
A3: card C > card A by A2, Th5;
C is StableSet of R by Th16;
hence contradiction by A1, A3; ::_thesis: verum
end;
end;
definition
let R be with_finite_stability# RelStr ;
func stability# R -> Nat means :Def6: :: DILWORTH:def 6
( ex A being finite StableSet of R st card A = it & ( for T being finite StableSet of R holds card T <= it ) );
existence
ex b1 being Nat st
( ex A being finite StableSet of R st card A = b1 & ( for T being finite StableSet of R holds card T <= b1 ) )
proof
consider A being finite StableSet of R such that
A1: for B being finite StableSet of R holds card A >= card B by Def5;
take itt = card A; ::_thesis: ( ex A being finite StableSet of R st card A = itt & ( for T being finite StableSet of R holds card T <= itt ) )
thus ex A being finite StableSet of R st card A = itt ; ::_thesis: for T being finite StableSet of R holds card T <= itt
let T be finite StableSet of R; ::_thesis: card T <= itt
thus card T <= itt by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Nat st ex A being finite StableSet of R st card A = b1 & ( for T being finite StableSet of R holds card T <= b1 ) & ex A being finite StableSet of R st card A = b2 & ( for T being finite StableSet of R holds card T <= b2 ) holds
b1 = b2
proof
let it1, it2 be Nat; ::_thesis: ( ex A being finite StableSet of R st card A = it1 & ( for T being finite StableSet of R holds card T <= it1 ) & ex A being finite StableSet of R st card A = it2 & ( for T being finite StableSet of R holds card T <= it2 ) implies it1 = it2 )
assume that
A2: ex S1 being finite StableSet of R st card S1 = it1 and
A3: for T being finite StableSet of R holds card T <= it1 and
A4: ex S2 being finite StableSet of R st card S2 = it2 and
A5: for T being finite StableSet of R holds card T <= it2 ; ::_thesis: it1 = it2
consider S1 being finite StableSet of R such that
A6: card S1 = it1 by A2;
consider S2 being finite StableSet of R such that
A7: card S2 = it2 by A4;
( it1 <= it2 & it2 <= it1 ) by A3, A5, A6, A7;
hence it1 = it2 by XXREAL_0:1; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines stability# DILWORTH:def_6_:_
for R being with_finite_stability# RelStr
for b2 being Nat holds
( b2 = stability# R iff ( ex A being finite StableSet of R st card A = b2 & ( for T being finite StableSet of R holds card T <= b2 ) ) );
registration
let R be empty RelStr ;
cluster stability# R -> empty ;
coherence
stability# R is empty
proof
for T being StableSet of R holds card T <= card ({} R) ;
hence stability# R is empty by Def6; ::_thesis: verum
end;
end;
registration
let R be non empty with_finite_stability# RelStr ;
cluster stability# R -> positive ;
coherence
stability# R is positive
proof
card { the Element of R} <= stability# R by Def6;
hence stability# R is positive ; ::_thesis: verum
end;
end;
theorem Th20: :: DILWORTH:20
for R being non empty with_finite_stability# RelStr st [#] R is Clique of R holds
stability# R = 1
proof
let R be non empty with_finite_stability# RelStr ; ::_thesis: ( [#] R is Clique of R implies stability# R = 1 )
assume A1: [#] R is Clique of R ; ::_thesis: stability# R = 1
A2: stability# R >= 0 + 1 by NAT_1:13;
consider A being finite StableSet of R such that
A3: card A = stability# R by Def6;
assume stability# R <> 1 ; ::_thesis: contradiction
then card A > 1 by A2, A3, XXREAL_0:1;
then consider a, b being set such that
A4: a in A and
A5: b in A and
A6: a <> b by NAT_1:59;
thus contradiction by A4, A5, A6, A1, Th15; ::_thesis: verum
end;
theorem Th21: :: DILWORTH:21
for R being with_finite_stability# RelStr st stability# R = 1 holds
[#] R is Clique of R
proof
let R be with_finite_stability# RelStr ; ::_thesis: ( stability# R = 1 implies [#] R is Clique of R )
assume A1: stability# R = 1 ; ::_thesis: [#] R is Clique of R
set cR = the carrier of R;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_the_carrier_of_R_&_b_in_the_carrier_of_R_&_a_<>_b_&_not_a_<=_b_holds_
b_<=_a
let a, b be Element of R; ::_thesis: ( a in the carrier of R & b in the carrier of R & a <> b & not a <= b implies b <= a )
assume that
A2: a in the carrier of R and
b in the carrier of R and
A3: a <> b ; ::_thesis: ( a <= b or b <= a )
A4: not R is empty by A2;
assume ( not a <= b & not b <= a ) ; ::_thesis: contradiction
then A5: {a,b} is StableSet of R by A4, Th14;
card {a,b} = 2 by A3, CARD_2:57;
hence contradiction by A1, Def6, A5; ::_thesis: verum
end;
hence [#] R is Clique of R by Th6; ::_thesis: verum
end;
registration
cluster with_finite_clique# with_finite_stability# -> finite for RelStr ;
coherence
for b1 being RelStr st b1 is with_finite_clique# & b1 is with_finite_stability# holds
b1 is finite
proof
let R be RelStr ; ::_thesis: ( R is with_finite_clique# & R is with_finite_stability# implies R is finite )
assume A1: R is with_finite_clique# ; ::_thesis: ( not R is with_finite_stability# or R is finite )
assume A2: R is with_finite_stability# ; ::_thesis: R is finite
assume A3: R is infinite ; ::_thesis: contradiction
reconsider R = R as with_finite_clique# with_finite_stability# RelStr by A1, A2;
consider C being finite Clique of R such that
A4: card C = clique# R by Def4;
consider An being finite StableSet of R such that
A5: card An = stability# R by Def6;
set h = clique# R;
set w = stability# R;
A6: 0 + 1 <= clique# R by A3, NAT_1:13;
A7: 0 + 1 <= stability# R by A3, NAT_1:13;
set cR = the carrier of R;
A8: the carrier of R = [#] R ;
percases ( clique# R = 1 or stability# R = 1 or ( clique# R > 1 & stability# R > 1 ) ) by A6, A7, XXREAL_0:1;
suppose clique# R = 1 ; ::_thesis: contradiction
then A9: the carrier of R is StableSet of R by A8, Th19;
consider Y being finite Subset of the carrier of R such that
A10: card Y > stability# R by A3, Th5;
Y is StableSet of R by A9, Th16;
hence contradiction by A10, Def6; ::_thesis: verum
end;
suppose stability# R = 1 ; ::_thesis: contradiction
then A11: the carrier of R is Clique of R by A8, Th21;
consider Y being finite Subset of the carrier of R such that
A12: card Y > clique# R by A3, Th5;
Y is Clique of R by A11, Th9;
hence contradiction by A12, Def4; ::_thesis: verum
end;
supposeA13: ( clique# R > 1 & stability# R > 1 ) ; ::_thesis: contradiction
set m = (max ((clique# R),(stability# R))) + 1;
reconsider m = (max ((clique# R),(stability# R))) + 1 as Nat ;
consider r being Nat such that
A14: for X being finite set
for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds
ex S being Subset of X st
( card S >= m & S is_homogeneous_for P ) by RAMSEY_1:17;
consider Y being finite Subset of R such that
A15: card Y > r by A3, Th5;
set X = (Y \/ An) \/ C;
reconsider X = (Y \/ An) \/ C as finite Subset of R ;
( Y c= Y \/ An & Y \/ An c= (Y \/ An) \/ C ) by XBOOLE_1:7;
then A16: card Y <= card X by NAT_1:43, XBOOLE_1:1;
set A = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ;
set B = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ;
set E = the_subsets_of_card (2,X);
set P = { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } };
A17: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } c= the_subsets_of_card (2,X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or x in the_subsets_of_card (2,X) )
assume x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; ::_thesis: x in the_subsets_of_card (2,X)
then consider xx, yy being Element of R such that
A18: {xx,yy} = x and
A19: xx <> yy and
A20: xx in X and
A21: yy in X and
( xx <= yy or yy <= xx ) ;
( x is Subset of X & card x = 2 ) by A18, A19, A20, A21, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; ::_thesis: verum
end;
A22: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } c= the_subsets_of_card (2,X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } or x in the_subsets_of_card (2,X) )
assume x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: x in the_subsets_of_card (2,X)
then consider xx, yy being Element of R such that
A23: {xx,yy} = x and
A24: xx <> yy and
A25: xx in X and
A26: yy in X and
( not xx <= yy & not yy <= xx ) ;
( x is Subset of X & card x = 2 ) by A23, A24, A25, A26, CARD_2:57, ZFMISC_1:32;
hence x in the_subsets_of_card (2,X) ; ::_thesis: verum
end;
A27: ( { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } & { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ) by TARSKI:def_2;
A28: now__::_thesis:_not__{__{x,y}_where_x,_y_is_Element_of_R_:_(_x_<>_y_&_x_in_X_&_y_in_X_&_(_x_<=_y_or_y_<=_x_)_)__}__=__{__{x,y}_where_x,_y_is_Element_of_R_:_(_x_<>_y_&_x_in_X_&_y_in_X_&_not_x_<=_y_&_not_y_<=_x_)__}_
assume A29: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: contradiction
consider a, b being set such that
A30: a in An and
A31: b in An and
A32: a <> b by A13, A5, NAT_1:59;
reconsider a = a, b = b as Element of R by A30, A31;
A33: ( not a <= b & not b <= a ) by A30, A31, A32, Def2;
( a in Y \/ An & b in Y \/ An ) by A30, A31, XBOOLE_0:def_3;
then ( a in X & b in X ) by XBOOLE_0:def_3;
then {a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A33, A32;
then consider aa, bb being Element of R such that
A34: {a,b} = {aa,bb} and
( aa <> bb & aa in X & bb in X ) and
A35: ( aa <= bb or bb <= aa ) by A29;
( ( a = aa & b = bb ) or ( a = bb & b = aa ) ) by A34, ZFMISC_1:6;
hence contradiction by A35, A30, A31, A32, Def2; ::_thesis: verum
end;
A36: { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } c= bool (the_subsets_of_card (2,X))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or x in bool (the_subsets_of_card (2,X)) )
assume x in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: x in bool (the_subsets_of_card (2,X))
then x c= the_subsets_of_card (2,X) by A17, A22, TARSKI:def_2;
hence x in bool (the_subsets_of_card (2,X)) ; ::_thesis: verum
end;
A37: union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } = the_subsets_of_card (2,X)
proof
thus union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } c= the_subsets_of_card (2,X) :: according to XBOOLE_0:def_10 ::_thesis: the_subsets_of_card (2,X) c= union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or x in the_subsets_of_card (2,X) )
assume x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: x in the_subsets_of_card (2,X)
then consider Y being set such that
A38: x in Y and
A39: Y in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } by TARSKI:def_4;
( Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by A39, TARSKI:def_2;
hence x in the_subsets_of_card (2,X) by A38, A17, A22; ::_thesis: verum
end;
thus the_subsets_of_card (2,X) c= union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_subsets_of_card (2,X) or x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } )
assume x in the_subsets_of_card (2,X) ; ::_thesis: x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }
then consider xx being Subset of X such that
A40: x = xx and
A41: card xx = 2 ;
consider a, b being set such that
A42: a <> b and
A43: xx = {a,b} by A41, CARD_2:60;
( a in xx & b in xx ) by A43, TARSKI:def_2;
then ( a in X & b in X ) ;
then reconsider a = a, b = b as Element of R ;
A44: ( a in xx & b in xx ) by A43, TARSKI:def_2;
( ( not a <= b & not b <= a ) or a <= b or b <= a ) ;
then ( {a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or {a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by A44, A42;
hence x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } by A40, A43, A27, TARSKI:def_4; ::_thesis: verum
end;
end;
for a being Subset of (the_subsets_of_card (2,X)) st a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } holds
( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) )
proof
let a be Subset of (the_subsets_of_card (2,X)); ::_thesis: ( a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } implies ( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) ) )
assume A45: a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: ( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) )
thus a <> {} ::_thesis: for b being Subset of (the_subsets_of_card (2,X)) holds
( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b )
proof
percases ( a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by A45, TARSKI:def_2;
supposeA46: a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; ::_thesis: a <> {}
consider aa, bb being set such that
A47: aa in C and
A48: bb in C and
A49: aa <> bb by A13, A4, NAT_1:59;
reconsider aa = aa, bb = bb as Element of R by A47, A48;
A50: ( aa <= bb or bb <= aa ) by A47, A48, A49, Th6;
( aa in (Y \/ An) \/ C & bb in (Y \/ An) \/ C ) by A47, A48, XBOOLE_0:def_3;
then {aa,bb} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by A50, A49;
hence a <> {} by A46; ::_thesis: verum
end;
supposeA51: a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: a <> {}
consider aa, bb being set such that
A52: aa in An and
A53: bb in An and
A54: aa <> bb by A13, A5, NAT_1:59;
reconsider aa = aa, bb = bb as Element of R by A52, A53;
A55: ( not aa <= bb & not bb <= aa ) by A52, A53, A54, Def2;
( aa in Y \/ An & bb in Y \/ An ) by A52, A53, XBOOLE_0:def_3;
then ( aa in X & bb in X ) by XBOOLE_0:def_3;
then {aa,bb} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A55, A54;
hence a <> {} by A51; ::_thesis: verum
end;
end;
end;
let b be Subset of (the_subsets_of_card (2,X)); ::_thesis: ( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b )
assume A56: b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: ( a = b or a misses b )
assume A57: a <> b ; ::_thesis: a misses b
assume A58: a meets b ; ::_thesis: contradiction
( ( a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) & ( b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) ) by A45, A56, TARSKI:def_2;
then { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } <> {} by A57, A58, XBOOLE_0:def_7;
then consider x being set such that
A59: x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by XBOOLE_0:def_1;
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by A59, XBOOLE_0:def_4;
then consider xx, yy being Element of R such that
A60: {xx,yy} = x and
( xx <> yy & xx in X & yy in X ) and
A61: ( xx <= yy or yy <= xx ) ;
x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A59, XBOOLE_0:def_4;
then consider x2, y2 being Element of R such that
A62: {x2,y2} = x and
( x2 <> y2 & x2 in X & y2 in X ) and
A63: ( not x2 <= y2 & not y2 <= x2 ) ;
( ( xx = x2 & yy = y2 ) or ( xx = y2 & yy = x2 ) ) by A60, A62, ZFMISC_1:6;
hence contradiction by A61, A63; ::_thesis: verum
end;
then reconsider P = { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } as a_partition of the_subsets_of_card (2,X) by A37, A36, EQREL_1:def_4;
card P = 2 by A28, CARD_2:57;
then consider S being Subset of X such that
A64: card S >= m and
A65: S is_homogeneous_for P by A16, A14, A15, XXREAL_0:2;
reconsider S = S as finite Subset of R by XBOOLE_1:1;
max ((clique# R),(stability# R)) >= clique# R by XXREAL_0:25;
then m > clique# R by NAT_1:13;
then A66: card S > clique# R by A64, XXREAL_0:2;
max ((clique# R),(stability# R)) >= stability# R by XXREAL_0:25;
then m > stability# R by NAT_1:13;
then A67: card S > stability# R by A64, XXREAL_0:2;
consider p being Element of P such that
A68: the_subsets_of_card (2,S) c= p by A65, RAMSEY_1:def_1;
percases ( p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by TARSKI:def_2;
supposeA69: p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; ::_thesis: contradiction
now__::_thesis:_for_x,_y_being_Element_of_R_st_x_in_S_&_y_in_S_&_x_<>_y_&_not_x_<=_y_holds_
y_<=_x
let x, y be Element of R; ::_thesis: ( x in S & y in S & x <> y & not x <= y implies y <= x )
assume that
A70: x in S and
A71: y in S and
A72: x <> y ; ::_thesis: ( x <= y or y <= x )
( {x,y} is Subset of S & card {x,y} = 2 ) by A70, A71, A72, CARD_2:57, ZFMISC_1:32;
then {x,y} in the_subsets_of_card (2,S) ;
then {x,y} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by A69, A68;
then consider xx, yy being Element of R such that
A73: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A74: ( xx <= yy or yy <= xx ) ;
( ( xx = x & yy = y ) or ( xx = y & yy = x ) ) by A73, ZFMISC_1:6;
hence ( x <= y or y <= x ) by A74; ::_thesis: verum
end;
then S is Clique of R by Th6;
hence contradiction by A66, Def4; ::_thesis: verum
end;
supposeA75: p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: contradiction
S is stable
proof
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) )
assume that
A76: x in S and
A77: y in S and
A78: x <> y ; ::_thesis: ( not x <= y & not y <= x )
( {x,y} is Subset of S & card {x,y} = 2 ) by A76, A77, A78, CARD_2:57, ZFMISC_1:32;
then {x,y} in the_subsets_of_card (2,S) ;
then {x,y} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A75, A68;
then consider xx, yy being Element of R such that
A79: {xx,yy} = {x,y} and
( xx <> yy & xx in X & yy in X ) and
A80: ( not xx <= yy & not yy <= xx ) ;
( ( xx = x & yy = y ) or ( xx = y & yy = x ) ) by A79, ZFMISC_1:6;
hence ( not x <= y & not y <= x ) by A80; ::_thesis: verum
end;
hence contradiction by A67, Def6; ::_thesis: verum
end;
end;
end;
end;
end;
end;
begin
definition
let R be RelStr ;
let X be Subset of R;
func Lower X -> Subset of R equals :: DILWORTH:def 7
X \/ (downarrow X);
coherence
X \/ (downarrow X) is Subset of R ;
func Upper X -> Subset of R equals :: DILWORTH:def 8
X \/ (uparrow X);
coherence
X \/ (uparrow X) is Subset of R ;
end;
:: deftheorem defines Lower DILWORTH:def_7_:_
for R being RelStr
for X being Subset of R holds Lower X = X \/ (downarrow X);
:: deftheorem defines Upper DILWORTH:def_8_:_
for R being RelStr
for X being Subset of R holds Upper X = X \/ (uparrow X);
theorem Th22: :: DILWORTH:22
for R being transitive antisymmetric RelStr
for A being StableSet of R
for z being set st z in Upper A & z in Lower A holds
z in A
proof
let R be transitive antisymmetric RelStr ; ::_thesis: for A being StableSet of R
for z being set st z in Upper A & z in Lower A holds
z in A
let A be StableSet of R; ::_thesis: for z being set st z in Upper A & z in Lower A holds
z in A
let z be set ; ::_thesis: ( z in Upper A & z in Lower A implies z in A )
assume that
A1: z in Upper A and
A2: z in Lower A ; ::_thesis: z in A
percases ( z in A or not z in A ) ;
suppose z in A ; ::_thesis: z in A
hence z in A ; ::_thesis: verum
end;
supposeA3: not z in A ; ::_thesis: z in A
then A4: z in uparrow A by A1, XBOOLE_0:def_3;
A5: z in downarrow A by A2, A3, XBOOLE_0:def_3;
reconsider y = z as Element of R by A1;
consider x being Element of R such that
A6: x <= y and
A7: x in A by A4, WAYBEL_0:def_16;
reconsider x9 = z as Element of R by A2;
consider y9 being Element of R such that
A8: x9 <= y9 and
A9: y9 in A by A5, WAYBEL_0:def_15;
x <= y9 by A6, A8, YELLOW_0:def_2;
then x = y9 by A7, A9, Def2;
hence z in A by A6, A7, A8, YELLOW_0:def_3; ::_thesis: verum
end;
end;
end;
theorem Th23: :: DILWORTH:23
for R being with_finite_stability# RelStr
for A being StableSet of R st card A = stability# R holds
(Upper A) \/ (Lower A) = [#] R
proof
let R be with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R st card A = stability# R holds
(Upper A) \/ (Lower A) = [#] R
let A be StableSet of R; ::_thesis: ( card A = stability# R implies (Upper A) \/ (Lower A) = [#] R )
assume A1: card A = stability# R ; ::_thesis: (Upper A) \/ (Lower A) = [#] R
set cP = the carrier of R;
the carrier of R c= (Upper A) \/ (Lower A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in (Upper A) \/ (Lower A) )
assume A2: x in the carrier of R ; ::_thesis: x in (Upper A) \/ (Lower A)
assume A3: not x in (Upper A) \/ (Lower A) ; ::_thesis: contradiction
reconsider x = x as Element of the carrier of R by A2;
A4: not x in Upper A by A3, XBOOLE_0:def_3;
then A5: not x in A by XBOOLE_0:def_3;
A6: not x in uparrow A by A4, XBOOLE_0:def_3;
not x in Lower A by A3, XBOOLE_0:def_3;
then A7: not x in downarrow A by XBOOLE_0:def_3;
set Ax = A \/ {x};
A8: {x} c= the carrier of R by A2, ZFMISC_1:31;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_A_\/_{x}_&_b_in_A_\/_{x}_&_a_<>_b_holds_
(_not_a_<=_b_&_not_b_<=_a_)
let a, b be Element of R; ::_thesis: ( a in A \/ {x} & b in A \/ {x} & a <> b implies ( not b1 <= b2 & not b2 <= b1 ) )
assume that
A9: a in A \/ {x} and
A10: b in A \/ {x} and
A11: a <> b ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 )
percases ( ( a in A & b in A ) or ( a in A & b in {x} ) or ( a in {x} & b in A ) or ( a in {x} & b in {x} ) ) by A9, A10, XBOOLE_0:def_3;
suppose ( a in A & b in A ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 )
hence ( not a <= b & not b <= a ) by A11, Def2; ::_thesis: verum
end;
supposeA12: ( a in A & b in {x} ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 )
then b = x by TARSKI:def_1;
hence ( not a <= b & not b <= a ) by A6, A7, A12, WAYBEL_0:def_15, WAYBEL_0:def_16; ::_thesis: verum
end;
supposeA13: ( a in {x} & b in A ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 )
then a = x by TARSKI:def_1;
hence ( not a <= b & not b <= a ) by A6, A7, A13, WAYBEL_0:def_15, WAYBEL_0:def_16; ::_thesis: verum
end;
suppose ( a in {x} & b in {x} ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 )
then ( a = x & b = x ) by TARSKI:def_1;
hence ( not a <= b & not b <= a ) by A11; ::_thesis: verum
end;
end;
end;
then A14: A \/ {x} is StableSet of R by A8, Def2, XBOOLE_1:8;
card (A \/ {x}) = (card A) + 1 by A5, CARD_2:41;
then card (A \/ {x}) > card A by NAT_1:13;
hence contradiction by Def6, A1, A14; ::_thesis: verum
end;
hence (Upper A) \/ (Lower A) = [#] R by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th24: :: DILWORTH:24
for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R
proof
let R be transitive RelStr ; ::_thesis: for x being Element of R
for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R
let x be Element of R; ::_thesis: for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R
let S be Subset of R; ::_thesis: ( x is_minimal_in Lower S implies x is_minimal_in [#] R )
assume A1: x is_minimal_in Lower S ; ::_thesis: x is_minimal_in [#] R
set cR = the carrier of R;
A2: x in Lower S by A1, WAYBEL_4:56;
assume not x is_minimal_in [#] R ; ::_thesis: contradiction
then consider y being Element of R such that
y in the carrier of R and
A3: y < x by A2, WAYBEL_4:56;
percases ( x in S or x in downarrow S ) by A2, XBOOLE_0:def_3;
supposeA4: x in S ; ::_thesis: contradiction
y <= x by A3, ORDERS_2:def_6;
then y in downarrow S by A4, WAYBEL_0:def_15;
then y in Lower S by XBOOLE_0:def_3;
hence contradiction by A1, A3, WAYBEL_4:56; ::_thesis: verum
end;
suppose x in downarrow S ; ::_thesis: contradiction
then consider x99 being Element of R such that
A5: x <= x99 and
A6: x99 in S by WAYBEL_0:def_15;
y <= x by A3, ORDERS_2:def_6;
then y <= x99 by A5, YELLOW_0:def_2;
then y in downarrow S by A6, WAYBEL_0:def_15;
then y in Lower S by XBOOLE_0:def_3;
hence contradiction by A1, A3, WAYBEL_4:56; ::_thesis: verum
end;
end;
end;
theorem Th25: :: DILWORTH:25
for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R
proof
let R be transitive RelStr ; ::_thesis: for x being Element of R
for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R
let x be Element of R; ::_thesis: for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R
let S be Subset of R; ::_thesis: ( x is_maximal_in Upper S implies x is_maximal_in [#] R )
assume A1: x is_maximal_in Upper S ; ::_thesis: x is_maximal_in [#] R
set cR = the carrier of R;
A2: x in Upper S by A1, WAYBEL_4:55;
assume not x is_maximal_in [#] R ; ::_thesis: contradiction
then consider y being Element of R such that
y in the carrier of R and
A3: x < y by A2, WAYBEL_4:55;
percases ( x in S or x in uparrow S ) by A2, XBOOLE_0:def_3;
supposeA4: x in S ; ::_thesis: contradiction
x <= y by A3, ORDERS_2:def_6;
then y in uparrow S by A4, WAYBEL_0:def_16;
then y in Upper S by XBOOLE_0:def_3;
hence contradiction by A1, A3, WAYBEL_4:55; ::_thesis: verum
end;
suppose x in uparrow S ; ::_thesis: contradiction
then consider x99 being Element of R such that
A5: x99 <= x and
A6: x99 in S by WAYBEL_0:def_16;
x <= y by A3, ORDERS_2:def_6;
then x99 <= y by A5, YELLOW_0:def_2;
then y in uparrow S by A6, WAYBEL_0:def_16;
then y in Upper S by XBOOLE_0:def_3;
hence contradiction by A1, A3, WAYBEL_4:55; ::_thesis: verum
end;
end;
end;
definition
let R be RelStr ;
set cR = the carrier of R;
func minimals R -> Subset of R means :Def9: :: DILWORTH:def 9
for x being Element of R holds
( x in it iff x is_minimal_in [#] R ) if not R is empty
otherwise it = {} ;
consistency
for b1 being Subset of R holds verum ;
existence
( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) )
proof
defpred S1[ set ] means ex a being Element of R st
( a = $1 & a is_minimal_in the carrier of R );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of R & S1[x] ) ) from XBOOLE_0:sch_1();
A2: now__::_thesis:_(_not_the_carrier_of_R_is_empty_implies_ex_X_being_Subset_of_R_st_
for_x_being_Element_of_R_holds_
(_x_in_X_iff_x_is_minimal_in_the_carrier_of_R_)_)
assume A3: not the carrier of R is empty ; ::_thesis: ex X being Subset of R st
for x being Element of R holds
( x in X iff x is_minimal_in the carrier of R )
for x being set st x in X holds
x in the carrier of R by A1;
then reconsider X = X as Subset of R by TARSKI:def_3;
take X = X; ::_thesis: for x being Element of R holds
( x in X iff x is_minimal_in the carrier of R )
let x be Element of R; ::_thesis: ( x in X iff x is_minimal_in the carrier of R )
( x in X implies S1[x] ) by A1;
hence ( x in X iff x is_minimal_in the carrier of R ) by A1, A3; ::_thesis: verum
end;
now__::_thesis:_ex_X_being_Subset_of_R_st_X_=_{}
reconsider X = {} as Subset of R by XBOOLE_1:2;
take X = X; ::_thesis: X = {}
thus X = {} ; ::_thesis: verum
end;
hence ( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of R holds
( ( not R is empty & ( for x being Element of R holds
( x in b1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds
( x in b2 iff x is_minimal_in [#] R ) ) implies b1 = b2 ) & ( R is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let it1, it2 be Subset of R; ::_thesis: ( ( not R is empty & ( for x being Element of R holds
( x in it1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds
( x in it2 iff x is_minimal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) )
now__::_thesis:_(_not_R_is_empty_&_(_for_x_being_Element_of_R_holds_
(_x_in_it1_iff_x_is_minimal_in_the_carrier_of_R_)_)_&_(_for_x_being_Element_of_R_holds_
(_x_in_it2_iff_x_is_minimal_in_the_carrier_of_R_)_)_implies_it1_=_it2_)
assume that
not R is empty and
A4: for x being Element of R holds
( x in it1 iff x is_minimal_in the carrier of R ) and
A5: for x being Element of R holds
( x in it2 iff x is_minimal_in the carrier of R ) ; ::_thesis: it1 = it2
now__::_thesis:_for_x_being_set_holds_
(_x_in_it1_iff_x_in_it2_)
let x be set ; ::_thesis: ( x in it1 iff x in it2 )
now__::_thesis:_(_(_x_in_it1_or_x_in_it2_)_implies_(_x_in_it1_&_x_in_it2_)_)
assume A6: ( x in it1 or x in it2 ) ; ::_thesis: ( x in it1 & x in it2 )
then reconsider x9 = x as Element of R ;
x9 is_minimal_in the carrier of R by A6, A4, A5;
hence ( x in it1 & x in it2 ) by A4, A5; ::_thesis: verum
end;
hence ( x in it1 iff x in it2 ) ; ::_thesis: verum
end;
hence it1 = it2 by TARSKI:1; ::_thesis: verum
end;
hence ( ( not R is empty & ( for x being Element of R holds
( x in it1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds
( x in it2 iff x is_minimal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) ) ; ::_thesis: verum
end;
func maximals R -> Subset of R means :Def10: :: DILWORTH:def 10
for x being Element of R holds
( x in it iff x is_maximal_in [#] R ) if not R is empty
otherwise it = {} ;
consistency
for b1 being Subset of R holds verum ;
existence
( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_maximal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) )
proof
defpred S1[ set ] means ex a being Element of R st
( a = $1 & a is_maximal_in the carrier of R );
consider X being set such that
A7: for x being set holds
( x in X iff ( x in the carrier of R & S1[x] ) ) from XBOOLE_0:sch_1();
A8: now__::_thesis:_(_not_the_carrier_of_R_is_empty_implies_ex_X_being_Subset_of_R_st_
for_x_being_Element_of_R_holds_
(_x_in_X_iff_x_is_maximal_in_the_carrier_of_R_)_)
assume A9: not the carrier of R is empty ; ::_thesis: ex X being Subset of R st
for x being Element of R holds
( x in X iff x is_maximal_in the carrier of R )
for x being set st x in X holds
x in the carrier of R by A7;
then reconsider X = X as Subset of R by TARSKI:def_3;
take X = X; ::_thesis: for x being Element of R holds
( x in X iff x is_maximal_in the carrier of R )
let x be Element of R; ::_thesis: ( x in X iff x is_maximal_in the carrier of R )
( x in X implies S1[x] ) by A7;
hence ( x in X iff x is_maximal_in the carrier of R ) by A7, A9; ::_thesis: verum
end;
now__::_thesis:_ex_X_being_Subset_of_R_st_X_=_{}
reconsider X = {} as Subset of R by XBOOLE_1:2;
take X = X; ::_thesis: X = {}
thus X = {} ; ::_thesis: verum
end;
hence ( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_maximal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) ) by A8; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of R holds
( ( not R is empty & ( for x being Element of R holds
( x in b1 iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds
( x in b2 iff x is_maximal_in [#] R ) ) implies b1 = b2 ) & ( R is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let it1, it2 be Subset of R; ::_thesis: ( ( not R is empty & ( for x being Element of R holds
( x in it1 iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds
( x in it2 iff x is_maximal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) )
now__::_thesis:_(_not_R_is_empty_&_(_for_x_being_Element_of_R_holds_
(_x_in_it1_iff_x_is_maximal_in_the_carrier_of_R_)_)_&_(_for_x_being_Element_of_R_holds_
(_x_in_it2_iff_x_is_maximal_in_the_carrier_of_R_)_)_implies_it1_=_it2_)
assume that
not R is empty and
A10: for x being Element of R holds
( x in it1 iff x is_maximal_in the carrier of R ) and
A11: for x being Element of R holds
( x in it2 iff x is_maximal_in the carrier of R ) ; ::_thesis: it1 = it2
now__::_thesis:_for_x_being_set_holds_
(_x_in_it1_iff_x_in_it2_)
let x be set ; ::_thesis: ( x in it1 iff x in it2 )
now__::_thesis:_(_(_x_in_it1_or_x_in_it2_)_implies_(_x_in_it1_&_x_in_it2_)_)
assume A12: ( x in it1 or x in it2 ) ; ::_thesis: ( x in it1 & x in it2 )
then reconsider x9 = x as Element of R ;
x9 is_maximal_in the carrier of R by A12, A10, A11;
hence ( x in it1 & x in it2 ) by A10, A11; ::_thesis: verum
end;
hence ( x in it1 iff x in it2 ) ; ::_thesis: verum
end;
hence it1 = it2 by TARSKI:1; ::_thesis: verum
end;
hence ( ( not R is empty & ( for x being Element of R holds
( x in it1 iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds
( x in it2 iff x is_maximal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines minimals DILWORTH:def_9_:_
for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = minimals R iff for x being Element of R holds
( x in b2 iff x is_minimal_in [#] R ) ) ) & ( R is empty implies ( b2 = minimals R iff b2 = {} ) ) );
:: deftheorem Def10 defines maximals DILWORTH:def_10_:_
for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = maximals R iff for x being Element of R holds
( x in b2 iff x is_maximal_in [#] R ) ) ) & ( R is empty implies ( b2 = maximals R iff b2 = {} ) ) );
registration
let R be non empty transitive antisymmetric with_finite_clique# RelStr ;
cluster maximals R -> non empty ;
coherence
not maximals R is empty
proof
set cP = the carrier of R;
set iP = the InternalRel of R;
consider CL being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card CL by Def3;
card { the Element of R} <= card CL by A1;
then CL <> {} ;
then consider y being Element of R such that
y in CL and
A2: y is_maximal_wrt CL, the InternalRel of R by BAGORDER:6;
A3: y is_maximal_in CL by A2, WAYBEL_4:def_24;
A4: the carrier of R = [#] R ;
now__::_thesis:_y_is_maximal_in_the_carrier_of_R
assume not y is_maximal_in the carrier of R ; ::_thesis: contradiction
then consider z being Element of R such that
z in the carrier of R and
A5: y < z by WAYBEL_4:55;
A6: y <= z by A5, ORDERS_2:def_6;
set C = CL \/ {z};
reconsider C = CL \/ {z} as finite Clique of R by A6, A3, Th11;
not z in CL by A3, A5, WAYBEL_4:55;
then card C = (card CL) + 1 by CARD_2:41;
then (card CL) + 1 <= (card CL) + 0 by A1;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
hence not maximals R is empty by A4, Def10; ::_thesis: verum
end;
cluster minimals R -> non empty ;
coherence
not minimals R is empty
proof
set cP = the carrier of R;
set iP = the InternalRel of R;
consider CL being finite Clique of R such that
A7: for D being finite Clique of R holds card D <= card CL by Def3;
card { the Element of R} <= card CL by A7;
then CL <> {} ;
then consider y being Element of R such that
y in CL and
A8: y is_minimal_wrt CL, the InternalRel of R by BAGORDER:7;
A9: y is_minimal_in CL by A8, WAYBEL_4:def_26;
A10: the carrier of R = [#] R ;
now__::_thesis:_y_is_minimal_in_the_carrier_of_R
assume not y is_minimal_in the carrier of R ; ::_thesis: contradiction
then consider z being Element of R such that
z in the carrier of R and
A11: z < y by WAYBEL_4:56;
A12: z <= y by A11, ORDERS_2:def_6;
set C = CL \/ {z};
reconsider C = CL \/ {z} as finite Clique of R by A12, A9, Th12;
not z in CL by A9, A11, WAYBEL_4:56;
then card C = (card CL) + 1 by CARD_2:41;
then (card CL) + 1 <= (card CL) + 0 by A7;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
hence not minimals R is empty by A10, Def9; ::_thesis: verum
end;
end;
registration
let R be RelStr ;
cluster minimals R -> stable ;
coherence
minimals R is stable
proof
set mR = minimals R;
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in minimals R & y in minimals R & x <> y implies ( not x <= y & not y <= x ) )
assume that
A1: x in minimals R and
A2: y in minimals R and
A3: x <> y ; ::_thesis: ( not x <= y & not y <= x )
A4: not R is empty by A1;
then y is_minimal_in [#] R by A2, Def9;
then not y > x by A1, WAYBEL_4:56;
hence not x <= y by A3, ORDERS_2:def_6; ::_thesis: not y <= x
x is_minimal_in [#] R by A1, A4, Def9;
then not x > y by A2, WAYBEL_4:56;
hence not y <= x by A3, ORDERS_2:def_6; ::_thesis: verum
end;
cluster maximals R -> stable ;
coherence
maximals R is stable
proof
set mR = maximals R;
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in maximals R & y in maximals R & x <> y implies ( not x <= y & not y <= x ) )
assume that
A5: x in maximals R and
A6: y in maximals R and
A7: x <> y ; ::_thesis: ( not x <= y & not y <= x )
A8: not R is empty by A5;
then x is_maximal_in [#] R by A5, Def10;
then not y > x by A6, WAYBEL_4:55;
hence not x <= y by A7, ORDERS_2:def_6; ::_thesis: not y <= x
y is_maximal_in [#] R by A6, A8, Def10;
then not x > y by A5, WAYBEL_4:55;
hence not y <= x by A7, ORDERS_2:def_6; ::_thesis: verum
end;
end;
theorem Th26: :: DILWORTH:26
for R being RelStr
for A being StableSet of R st not minimals R c= A holds
not minimals R c= Upper A
proof
let R be RelStr ; ::_thesis: for A being StableSet of R st not minimals R c= A holds
not minimals R c= Upper A
let A be StableSet of R; ::_thesis: ( not minimals R c= A implies not minimals R c= Upper A )
assume not minimals R c= A ; ::_thesis: not minimals R c= Upper A
then consider x being set such that
A1: x in minimals R and
A2: not x in A by TARSKI:def_3;
assume A3: minimals R c= Upper A ; ::_thesis: contradiction
reconsider x9 = x as Element of R by A1;
not R is empty by A1;
then A4: x9 is_minimal_in [#] R by A1, Def9;
x9 in uparrow A by A2, A1, A3, XBOOLE_0:def_3;
then consider x99 being Element of R such that
A5: x99 <= x9 and
A6: x99 in A by WAYBEL_0:def_16;
now__::_thesis:_not_x99_<>_x9
assume x99 <> x9 ; ::_thesis: contradiction
then x99 < x9 by A5, ORDERS_2:def_6;
hence contradiction by A1, A4, WAYBEL_4:56; ::_thesis: verum
end;
hence contradiction by A6, A2; ::_thesis: verum
end;
theorem Th27: :: DILWORTH:27
for R being RelStr
for A being StableSet of R st not maximals R c= A holds
not maximals R c= Lower A
proof
let R be RelStr ; ::_thesis: for A being StableSet of R st not maximals R c= A holds
not maximals R c= Lower A
let A be StableSet of R; ::_thesis: ( not maximals R c= A implies not maximals R c= Lower A )
assume A1: not maximals R c= A ; ::_thesis: not maximals R c= Lower A
consider x being set such that
A2: x in maximals R and
A3: not x in A by A1, TARSKI:def_3;
assume A4: maximals R c= Lower A ; ::_thesis: contradiction
reconsider x9 = x as Element of R by A2;
not R is empty by A2;
then A5: x9 is_maximal_in [#] R by A2, Def10;
x9 in downarrow A by A3, A2, A4, XBOOLE_0:def_3;
then consider x99 being Element of R such that
A6: x9 <= x99 and
A7: x99 in A by WAYBEL_0:def_15;
now__::_thesis:_not_x99_<>_x9
assume x99 <> x9 ; ::_thesis: contradiction
then x9 < x99 by A6, ORDERS_2:def_6;
hence contradiction by A2, A5, WAYBEL_4:55; ::_thesis: verum
end;
hence contradiction by A7, A3; ::_thesis: verum
end;
begin
registration
let R be RelStr ;
let X be finite Subset of R;
cluster subrelstr X -> finite ;
coherence
subrelstr X is finite by YELLOW_0:def_15;
end;
theorem Th28: :: DILWORTH:28
for R being RelStr
for S being Subset of R
for C being Clique of (subrelstr S) holds C is Clique of R
proof
let R be RelStr ; ::_thesis: for S being Subset of R
for C being Clique of (subrelstr S) holds C is Clique of R
let S be Subset of R; ::_thesis: for C being Clique of (subrelstr S) holds C is Clique of R
let C be Clique of (subrelstr S); ::_thesis: C is Clique of R
A1: the carrier of (subrelstr S) = S by YELLOW_0:def_15;
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 a9 = a, b9 = b as Element of (subrelstr S) by A2, A3;
( a9 <= b9 or b9 <= a9 ) by A2, A3, A4, Th6;
hence ( a <= b or b <= a ) by YELLOW_0:59; ::_thesis: verum
end;
hence C is Clique of R by A1, Th6, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th29: :: DILWORTH:29
for R being RelStr
for S being Subset of R
for C being Clique of R holds C /\ S is Clique of (subrelstr S)
proof
let R be RelStr ; ::_thesis: for S being Subset of R
for C being Clique of R holds C /\ S is Clique of (subrelstr S)
let S be Subset of R; ::_thesis: for C being Clique of R holds C /\ S is Clique of (subrelstr S)
let C be Clique of R; ::_thesis: C /\ S is Clique of (subrelstr S)
set sS = subrelstr S;
set CS = C /\ S;
A1: C /\ S c= S by XBOOLE_1:17;
A2: S = the carrier of (subrelstr S) by YELLOW_0:def_15;
now__::_thesis:_for_a,_b_being_Element_of_(subrelstr_S)_holds_
(_not_a_in_C_/\_S_or_not_b_in_C_/\_S_or_not_a_<>_b_or_a_<=_b_or_b_<=_a_)
let a, b be Element of (subrelstr S); ::_thesis: ( not a in C /\ S or not b in C /\ S or not a <> b or a <= b or b <= a )
assume A3: a in C /\ S ; ::_thesis: ( not b in C /\ S or not a <> b or a <= b or b <= a )
assume A4: b in C /\ S ; ::_thesis: ( not a <> b or a <= b or b <= a )
assume A5: a <> b ; ::_thesis: ( a <= b or b <= a )
A6: ( a in S & b in S ) by A3, A4, XBOOLE_0:def_4;
A7: not S is empty by A3;
not R is empty by A3;
then reconsider a9 = a, b9 = b as Element of R by A7, YELLOW_0:58;
( a9 in C & b9 in C ) by A3, A4, XBOOLE_0:def_4;
then ( a9 <= b9 or b9 <= a9 ) by A5, Th6;
hence ( a <= b or b <= a ) by A6, A2, YELLOW_0:60; ::_thesis: verum
end;
hence C /\ S is Clique of (subrelstr S) by Th6, A1, YELLOW_0:def_15; ::_thesis: verum
end;
theorem Th30: :: DILWORTH:30
for R being RelStr
for S being Subset of R
for A being StableSet of (subrelstr S) holds A is StableSet of R
proof
let R be RelStr ; ::_thesis: for S being Subset of R
for A being StableSet of (subrelstr S) holds A is StableSet of R
let S be Subset of R; ::_thesis: for A being StableSet of (subrelstr S) holds A is StableSet of R
let A be StableSet of (subrelstr S); ::_thesis: A is StableSet of R
set sS = subrelstr S;
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: A is StableSet of R
then the carrier of (subrelstr S) = {} by YELLOW_0:def_15;
then A = {} R ;
hence A is StableSet of R ; ::_thesis: verum
end;
supposeA1: not R is empty ; ::_thesis: A is StableSet of R
percases ( S is empty or not S is empty ) ;
suppose S is empty ; ::_thesis: A is StableSet of R
then the carrier of (subrelstr S) = {} by YELLOW_0:def_15;
then A = {} R ;
hence A is StableSet of R ; ::_thesis: verum
end;
supposeA2: not S is empty ; ::_thesis: A is StableSet of R
S = the carrier of (subrelstr S) by YELLOW_0:def_15;
then reconsider A = A as Subset of R by XBOOLE_1:1;
A is stable
proof
let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in A & y in A & x <> y implies ( not x <= y & not y <= x ) )
assume that
A3: x in A and
A4: y in A and
A5: x <> y ; ::_thesis: ( not x <= y & not y <= x )
reconsider x9 = x, y9 = y as Element of (subrelstr S) by A3, A4;
( not x9 <= y9 & not y9 <= x9 ) by A3, A4, A5, Def2;
hence ( not x <= y & not y <= x ) by A1, A2, YELLOW_0:60; ::_thesis: verum
end;
hence A is StableSet of R ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th31: :: DILWORTH:31
for R being RelStr
for S being Subset of R
for A being StableSet of R holds A /\ S is StableSet of (subrelstr S)
proof
let R be RelStr ; ::_thesis: for S being Subset of R
for A being StableSet of R holds A /\ S is StableSet of (subrelstr S)
let S be Subset of R; ::_thesis: for A being StableSet of R holds A /\ S is StableSet of (subrelstr S)
let A be StableSet of R; ::_thesis: A /\ S is StableSet of (subrelstr S)
set sS = subrelstr S;
set AS = A /\ S;
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S)
then A /\ S = {} (subrelstr S) ;
hence A /\ S is StableSet of (subrelstr S) ; ::_thesis: verum
end;
supposeA1: not R is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S)
percases ( S is empty or not S is empty ) ;
suppose S is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S)
then A /\ S = {} (subrelstr S) ;
hence A /\ S is StableSet of (subrelstr S) ; ::_thesis: verum
end;
supposeA2: not S is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S)
S = the carrier of (subrelstr S) by YELLOW_0:def_15;
then reconsider AS = A /\ S as Subset of (subrelstr S) by XBOOLE_1:17;
AS is stable
proof
let x, y be Element of (subrelstr S); :: according to DILWORTH:def_2 ::_thesis: ( x in AS & y in AS & x <> y implies ( not x <= y & not y <= x ) )
assume that
A3: x in AS and
A4: y in AS and
A5: x <> y ; ::_thesis: ( not x <= y & not y <= x )
reconsider x9 = x, y9 = y as Element of R by A1, A2, YELLOW_0:58;
A6: x9 in A by A3, XBOOLE_0:def_4;
y9 in A by A4, XBOOLE_0:def_4;
then ( not x9 <= y9 & not y9 <= x9 ) by A6, A5, Def2;
hence ( not x <= y & not y <= x ) by YELLOW_0:59; ::_thesis: verum
end;
hence A /\ S is StableSet of (subrelstr S) ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th32: :: DILWORTH:32
for R being RelStr
for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_maximal_in B holds
y is_maximal_in B
proof
let R be RelStr ; ::_thesis: for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_maximal_in B holds
y is_maximal_in B
let S be Subset of R; ::_thesis: for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_maximal_in B holds
y is_maximal_in B
let B be Subset of (subrelstr S); ::_thesis: for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_maximal_in B holds
y is_maximal_in B
let x be Element of (subrelstr S); ::_thesis: for y being Element of R st x = y & x is_maximal_in B holds
y is_maximal_in B
let y be Element of R; ::_thesis: ( x = y & x is_maximal_in B implies y is_maximal_in B )
assume that
A1: x = y and
A2: x is_maximal_in B ; ::_thesis: y is_maximal_in B
A3: x in B by A2, WAYBEL_4:55;
assume not y is_maximal_in B ; ::_thesis: contradiction
then consider z being Element of R such that
A4: z in B and
A5: y < z by A1, A3, WAYBEL_4:55;
A6: y <= z by A5, ORDERS_2:def_6;
reconsider z9 = z as Element of (subrelstr S) by A4;
x <= z9 by A4, A6, A1, YELLOW_0:60;
then x < z9 by A5, A1, ORDERS_2:def_6;
hence contradiction by A4, A2, WAYBEL_4:55; ::_thesis: verum
end;
theorem Th33: :: DILWORTH:33
for R being RelStr
for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
proof
let R be RelStr ; ::_thesis: for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let S be Subset of R; ::_thesis: for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let B be Subset of (subrelstr S); ::_thesis: for x being Element of (subrelstr S)
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let x be Element of (subrelstr S); ::_thesis: for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
let y be Element of R; ::_thesis: ( x = y & x is_minimal_in B implies y is_minimal_in B )
assume that
A1: x = y and
A2: x is_minimal_in B ; ::_thesis: y is_minimal_in B
A3: x in B by A2, WAYBEL_4:56;
assume not y is_minimal_in B ; ::_thesis: contradiction
then consider z being Element of R such that
A4: z in B and
A5: z < y by A1, A3, WAYBEL_4:56;
A6: z <= y by A5, ORDERS_2:def_6;
reconsider z9 = z as Element of (subrelstr S) by A4;
z9 <= x by A4, A6, A1, YELLOW_0:60;
then z9 < x by A5, A1, ORDERS_2:def_6;
hence contradiction by A4, A2, WAYBEL_4:56; ::_thesis: verum
end;
theorem Th34: :: DILWORTH:34
for R being transitive RelStr
for A being StableSet of R
for C being Clique of (subrelstr (Lower A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
proof
let R be transitive RelStr ; ::_thesis: for A being StableSet of R
for C being Clique of (subrelstr (Lower A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
let A be StableSet of R; ::_thesis: for C being Clique of (subrelstr (Lower A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
let C be Clique of (subrelstr (Lower A)); ::_thesis: for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
let a, b be Element of R; ::_thesis: ( a in A & a in C & b in C & not a = b implies b <= a )
assume that
A1: a in A and
A2: a in C and
A3: b in C ; ::_thesis: ( a = b or b <= a )
set ap = subrelstr (Lower A);
reconsider a9 = a as Element of (subrelstr (Lower A)) by A2;
A4: b in the carrier of (subrelstr (Lower A)) by A3;
reconsider b9 = b as Element of (subrelstr (Lower A)) by A3;
A5: b9 in Lower A by A4, YELLOW_0:def_15;
A6: C is Clique of R by Th28;
percases ( b9 in A or b9 in downarrow A ) by A5, XBOOLE_0:def_3;
suppose b9 in A ; ::_thesis: ( a = b or b <= a )
hence ( a = b or b <= a ) by A1, A2, A3, A6, Th15; ::_thesis: verum
end;
suppose b9 in downarrow A ; ::_thesis: ( a = b or b <= a )
then consider c being Element of R such that
A7: b <= c and
A8: c in A by WAYBEL_0:def_15;
percases ( a <> b or a = b ) ;
supposeA9: a <> b ; ::_thesis: ( a = b or b <= a )
percases ( a9 <= b9 or b9 <= a9 ) by A9, A2, A3, Th6;
suppose a9 <= b9 ; ::_thesis: ( a = b or b <= a )
then a <= b by YELLOW_0:59;
then a <= c by A7, YELLOW_0:def_2;
hence ( a = b or b <= a ) by A8, A7, A1, Def2; ::_thesis: verum
end;
suppose b9 <= a9 ; ::_thesis: ( a = b or b <= a )
hence ( a = b or b <= a ) by YELLOW_0:59; ::_thesis: verum
end;
end;
end;
suppose a = b ; ::_thesis: ( a = b or b <= a )
hence ( a = b or b <= a ) ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th35: :: DILWORTH:35
for R being transitive RelStr
for A being StableSet of R
for C being Clique of (subrelstr (Upper A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
proof
let R be transitive RelStr ; ::_thesis: for A being StableSet of R
for C being Clique of (subrelstr (Upper A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
let A be StableSet of R; ::_thesis: for C being Clique of (subrelstr (Upper A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
let C be Clique of (subrelstr (Upper A)); ::_thesis: for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
let a, b be Element of R; ::_thesis: ( a in A & a in C & b in C & not a = b implies a <= b )
assume that
A1: a in A and
A2: a in C and
A3: b in C ; ::_thesis: ( a = b or a <= b )
set ap = subrelstr (Upper A);
reconsider a9 = a as Element of (subrelstr (Upper A)) by A2;
A4: b in the carrier of (subrelstr (Upper A)) by A3;
reconsider b9 = b as Element of (subrelstr (Upper A)) by A3;
A5: b9 in Upper A by A4, YELLOW_0:def_15;
A6: C is Clique of R by Th28;
percases ( b9 in A or b9 in uparrow A ) by A5, XBOOLE_0:def_3;
suppose b9 in A ; ::_thesis: ( a = b or a <= b )
hence ( a = b or a <= b ) by A1, A2, A3, A6, Th15; ::_thesis: verum
end;
suppose b9 in uparrow A ; ::_thesis: ( a = b or a <= b )
then consider c being Element of R such that
A7: c <= b and
A8: c in A by WAYBEL_0:def_16;
percases ( a <> b or a = b ) ;
supposeA9: a <> b ; ::_thesis: ( a = b or a <= b )
percases ( a9 <= b9 or b9 <= a9 ) by A9, A2, A3, Th6;
suppose a9 <= b9 ; ::_thesis: ( a = b or a <= b )
hence ( a = b or a <= b ) by YELLOW_0:59; ::_thesis: verum
end;
suppose b9 <= a9 ; ::_thesis: ( a = b or a <= b )
then b <= a by YELLOW_0:59;
then c <= a by A7, YELLOW_0:def_2;
hence ( a = b or a <= b ) by A8, A7, A1, Def2; ::_thesis: verum
end;
end;
end;
suppose a = b ; ::_thesis: ( a = b or a <= b )
hence ( a = b or a <= b ) ; ::_thesis: verum
end;
end;
end;
end;
end;
registration
let R be with_finite_clique# RelStr ;
let S be Subset of R;
cluster subrelstr S -> with_finite_clique# ;
coherence
subrelstr S is with_finite_clique#
proof
consider C being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card C by Def3;
set sS = subrelstr S;
defpred S1[ Nat] means ex c being finite Clique of (subrelstr S) st card c = R;
A2: for k being Nat st S1[k] holds
k <= card C
proof
let k be Nat; ::_thesis: ( S1[k] implies k <= card C )
assume S1[k] ; ::_thesis: k <= card C
then consider c being finite Clique of (subrelstr S) such that
A3: card c = k ;
c is finite Clique of R by Th28;
hence k <= card C by A3, A1; ::_thesis: verum
end;
card ({} (subrelstr S)) = 0 ;
then A4: ex k being Nat st S1[k] ;
consider k being Nat such that
A5: S1[k] and
A6: for n being Nat st S1[n] holds
n <= k from NAT_1:sch_6(A2, A4);
consider c being finite Clique of (subrelstr S) such that
A7: card c = k by A5;
for D being finite Clique of (subrelstr S) holds card D <= card c by A7, A6;
hence subrelstr S is with_finite_clique# by Def3; ::_thesis: verum
end;
end;
registration
let R be with_finite_stability# RelStr ;
let S be Subset of R;
cluster subrelstr S -> with_finite_stability# ;
coherence
subrelstr S is with_finite_stability#
proof
consider A being finite StableSet of R such that
A1: for B being finite StableSet of R holds card A >= card B by Def5;
assume A2: not subrelstr S is with_finite_stability# ; ::_thesis: contradiction
defpred S1[ Nat] means ex C being finite StableSet of (subrelstr S) st
( card C = R & ex B being finite StableSet of (subrelstr S) st R < card B );
A3: S1[ 0 ]
proof
reconsider C = {} (subrelstr S) as finite StableSet of (subrelstr S) ;
take C ; ::_thesis: ( card C = 0 & ex B being finite StableSet of (subrelstr S) st 0 < card B )
thus card C = 0 ; ::_thesis: ex B being finite StableSet of (subrelstr S) st 0 < card B
hence ex B being finite StableSet of (subrelstr S) st 0 < card B by A2, Def5; ::_thesis: verum
end;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
given C being finite StableSet of (subrelstr S) such that card C = n and
A5: ex B being finite StableSet of (subrelstr S) st n < card B ; ::_thesis: S1[n + 1]
consider B being finite Subset of (subrelstr S) such that
A6: ( n < card B & B is StableSet of (subrelstr S) ) by A5;
n + 1 <= card B by A6, NAT_1:13;
then consider BB being finite StableSet of (subrelstr S) such that
A7: card BB = n + 1 by A6, Th17;
take BB ; ::_thesis: ( card BB = n + 1 & ex B being finite StableSet of (subrelstr S) st n + 1 < card B )
thus card BB = n + 1 by A7; ::_thesis: ex B being finite StableSet of (subrelstr S) st n + 1 < card B
consider Bb being finite StableSet of (subrelstr S) such that
A8: card BB < card Bb by A2, Def5;
take Bb ; ::_thesis: n + 1 < card Bb
thus n + 1 < card Bb by A8, A7; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A4);
then consider C being finite StableSet of (subrelstr S) such that
card C = card A and
A9: ex B being finite StableSet of (subrelstr S) st card A < card B ;
consider B being finite StableSet of (subrelstr S) such that
A10: card A < card B by A9;
B is StableSet of R by Th30;
hence contradiction by A1, A10; ::_thesis: verum
end;
end;
theorem Th36: :: DILWORTH:36
for R being non empty transitive antisymmetric with_finite_clique# RelStr
for x being Element of R ex y being Element of R st
( y is_minimal_in [#] R & ( y = x or y < x ) )
proof
let R be non empty transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for x being Element of R ex y being Element of R st
( y is_minimal_in [#] R & ( y = x or y < x ) )
let x be Element of R; ::_thesis: ex y being Element of R st
( y is_minimal_in [#] R & ( y = x or y < x ) )
set sx = Lower {x};
set sL = subrelstr (Lower {x});
reconsider sL = subrelstr (Lower {x}) as non empty transitive antisymmetric with_finite_clique# RelStr ;
consider y being set such that
A1: y in minimals sL by XBOOLE_0:def_1;
reconsider y = y as Element of sL by A1;
A2: [#] sL = Lower {x} by YELLOW_0:def_15;
then A3: y is_minimal_in Lower {x} by A1, Def9;
reconsider y9 = y as Element of R by YELLOW_0:58;
take y9 ; ::_thesis: ( y9 is_minimal_in [#] R & ( y9 = x or y9 < x ) )
Lower {x} c= the carrier of sL by YELLOW_0:def_15;
hence y9 is_minimal_in [#] R by A3, Th33, Th24; ::_thesis: ( y9 = x or y9 < x )
percases ( y9 = x or y9 <> x ) ;
suppose y9 = x ; ::_thesis: ( y9 = x or y9 < x )
hence ( y9 = x or y9 < x ) ; ::_thesis: verum
end;
suppose y9 <> x ; ::_thesis: ( y9 = x or y9 < x )
then not y9 in {x} by TARSKI:def_1;
then y9 in downarrow x by A2, XBOOLE_0:def_3;
then y9 <= x by WAYBEL_0:17;
hence ( y9 = x or y9 < x ) by ORDERS_2:def_6; ::_thesis: verum
end;
end;
end;
theorem :: DILWORTH:37
for R being transitive antisymmetric with_finite_clique# RelStr holds Upper (minimals R) = [#] R
proof
let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: Upper (minimals R) = [#] R
set ap = Upper (minimals R);
set cR = the carrier of R;
the carrier of R c= Upper (minimals R)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in Upper (minimals R) )
assume A1: x in the carrier of R ; ::_thesis: x in Upper (minimals R)
then reconsider x9 = x as Element of R ;
A2: not R is empty by A1;
then consider y being Element of R such that
A3: y is_minimal_in [#] R and
A4: ( y = x9 or y < x9 ) by Th36;
A5: y in minimals R by A3, A2, Def9;
percases ( x9 = y or y < x9 ) by A4;
suppose x9 = y ; ::_thesis: x in Upper (minimals R)
hence x in Upper (minimals R) by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose y < x9 ; ::_thesis: x in Upper (minimals R)
then y <= x9 by ORDERS_2:def_6;
then x in uparrow (minimals R) by A5, WAYBEL_0:def_16;
hence x in Upper (minimals R) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence Upper (minimals R) = [#] R by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th38: :: DILWORTH:38
for R being non empty transitive antisymmetric with_finite_clique# RelStr
for x being Element of R ex y being Element of R st
( y is_maximal_in [#] R & ( y = x or x < y ) )
proof
let R be non empty transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for x being Element of R ex y being Element of R st
( y is_maximal_in [#] R & ( y = x or x < y ) )
let x be Element of R; ::_thesis: ex y being Element of R st
( y is_maximal_in [#] R & ( y = x or x < y ) )
set ax = Upper {x};
set sU = subrelstr (Upper {x});
reconsider sU = subrelstr (Upper {x}) as non empty transitive antisymmetric with_finite_clique# RelStr ;
consider y being set such that
A1: y in maximals sU by XBOOLE_0:def_1;
reconsider y = y as Element of sU by A1;
A2: [#] sU = Upper {x} by YELLOW_0:def_15;
then A3: y is_maximal_in Upper {x} by A1, Def10;
reconsider y9 = y as Element of R by YELLOW_0:58;
take y9 ; ::_thesis: ( y9 is_maximal_in [#] R & ( y9 = x or x < y9 ) )
Upper {x} c= the carrier of sU by YELLOW_0:def_15;
hence y9 is_maximal_in [#] R by A3, Th32, Th25; ::_thesis: ( y9 = x or x < y9 )
percases ( y9 = x or y9 <> x ) ;
suppose y9 = x ; ::_thesis: ( y9 = x or x < y9 )
hence ( y9 = x or x < y9 ) ; ::_thesis: verum
end;
suppose y9 <> x ; ::_thesis: ( y9 = x or x < y9 )
then not y9 in {x} by TARSKI:def_1;
then y9 in uparrow x by A2, XBOOLE_0:def_3;
then x <= y9 by WAYBEL_0:18;
hence ( y9 = x or x < y9 ) by ORDERS_2:def_6; ::_thesis: verum
end;
end;
end;
theorem :: DILWORTH:39
for R being transitive antisymmetric with_finite_clique# RelStr holds Lower (maximals R) = [#] R
proof
let P be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: Lower (maximals P) = [#] P
set ap = Lower (maximals P);
set cP = the carrier of P;
the carrier of P c= Lower (maximals P)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of P or x in Lower (maximals P) )
assume A1: x in the carrier of P ; ::_thesis: x in Lower (maximals P)
then reconsider x9 = x as Element of P ;
A2: not P is empty by A1;
then consider y being Element of P such that
A3: y is_maximal_in [#] P and
A4: ( y = x9 or y > x9 ) by Th38;
A5: y in maximals P by A3, A2, Def10;
percases ( x9 = y or y > x9 ) by A4;
suppose x9 = y ; ::_thesis: x in Lower (maximals P)
hence x in Lower (maximals P) by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose y > x9 ; ::_thesis: x in Lower (maximals P)
then x9 <= y by ORDERS_2:def_6;
then x in downarrow (maximals P) by A5, WAYBEL_0:def_15;
hence x in Lower (maximals P) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence Lower (maximals P) = [#] P by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th40: :: DILWORTH:40
for R being transitive antisymmetric with_finite_clique# RelStr
for A being StableSet of R st minimals R c= A holds
A = minimals R
proof
let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for A being StableSet of R st minimals R c= A holds
A = minimals R
let A be StableSet of R; ::_thesis: ( minimals R c= A implies A = minimals R )
assume A1: minimals R c= A ; ::_thesis: A = minimals R
A c= minimals R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in minimals R )
assume A2: x in A ; ::_thesis: x in minimals R
then A3: not R is empty ;
reconsider x9 = x as Element of R by A2;
consider y being Element of R such that
A4: y is_minimal_in [#] R and
A5: ( y = x9 or y < x9 ) by A3, Th36;
A6: ( y = x9 or y <= x9 ) by A5, ORDERS_2:def_6;
y in minimals R by A3, A4, Def9;
hence x in minimals R by A1, A2, A6, Def2; ::_thesis: verum
end;
hence A = minimals R by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th41: :: DILWORTH:41
for R being transitive antisymmetric with_finite_clique# RelStr
for A being StableSet of R st maximals R c= A holds
A = maximals R
proof
let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for A being StableSet of R st maximals R c= A holds
A = maximals R
let A be StableSet of R; ::_thesis: ( maximals R c= A implies A = maximals R )
assume A1: maximals R c= A ; ::_thesis: A = maximals R
A c= maximals R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in maximals R )
assume A2: x in A ; ::_thesis: x in maximals R
then A3: not R is empty ;
reconsider x9 = x as Element of R by A2;
consider y being Element of R such that
A4: y is_maximal_in [#] R and
A5: ( y = x9 or x9 < y ) by A3, Th38;
A6: ( y = x9 or x9 <= y ) by A5, ORDERS_2:def_6;
y in maximals R by A3, A4, Def10;
hence x in maximals R by A1, A2, A6, Def2; ::_thesis: verum
end;
hence A = maximals R by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th42: :: DILWORTH:42
for R being with_finite_clique# RelStr
for S being Subset of R holds clique# (subrelstr S) <= clique# R
proof
let R be with_finite_clique# RelStr ; ::_thesis: for S being Subset of R holds clique# (subrelstr S) <= clique# R
let S be Subset of R; ::_thesis: clique# (subrelstr S) <= clique# R
set s = subrelstr S;
consider c being finite Clique of (subrelstr S) such that
A1: card c = clique# (subrelstr S) by Def4;
c is Clique of R by Th28;
hence clique# (subrelstr S) <= clique# R by Def4, A1; ::_thesis: verum
end;
theorem :: DILWORTH:43
for R being with_finite_clique# RelStr
for C being Clique of R
for S being Subset of R st card C = clique# R & C c= S holds
clique# (subrelstr S) = clique# R
proof
let R be with_finite_clique# RelStr ; ::_thesis: for C being Clique of R
for S being Subset of R st card C = clique# R & C c= S holds
clique# (subrelstr S) = clique# R
let C be Clique of R; ::_thesis: for S being Subset of R st card C = clique# R & C c= S holds
clique# (subrelstr S) = clique# R
let S be Subset of R; ::_thesis: ( card C = clique# R & C c= S implies clique# (subrelstr S) = clique# R )
assume that
A1: card C = clique# R and
A2: C c= S ; ::_thesis: clique# (subrelstr S) = clique# R
C = C /\ S by A2, XBOOLE_1:28;
then A3: C is Clique of (subrelstr S) by Th29;
consider Cs being Clique of (subrelstr S) such that
A4: card Cs = clique# (subrelstr S) by Def4;
A5: card C <= card Cs by A3, A4, Def4;
clique# (subrelstr S) <= clique# R by Th42;
hence clique# (subrelstr S) = clique# R by A4, A1, A5, XXREAL_0:1; ::_thesis: verum
end;
theorem Th44: :: DILWORTH:44
for R being with_finite_stability# RelStr
for S being Subset of R holds stability# (subrelstr S) <= stability# R
proof
let R be with_finite_stability# RelStr ; ::_thesis: for S being Subset of R holds stability# (subrelstr S) <= stability# R
let S be Subset of R; ::_thesis: stability# (subrelstr S) <= stability# R
consider As being StableSet of (subrelstr S) such that
A1: card As = stability# (subrelstr S) by Def6;
As is StableSet of R by Th30;
hence stability# (subrelstr S) <= stability# R by A1, Def6; ::_thesis: verum
end;
theorem Th45: :: DILWORTH:45
for R being with_finite_stability# RelStr
for A being StableSet of R
for S being Subset of R st card A = stability# R & A c= S holds
stability# (subrelstr S) = stability# R
proof
let R be with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R
for S being Subset of R st card A = stability# R & A c= S holds
stability# (subrelstr S) = stability# R
let A be StableSet of R; ::_thesis: for S being Subset of R st card A = stability# R & A c= S holds
stability# (subrelstr S) = stability# R
let S be Subset of R; ::_thesis: ( card A = stability# R & A c= S implies stability# (subrelstr S) = stability# R )
assume that
A1: card A = stability# R and
A2: A c= S ; ::_thesis: stability# (subrelstr S) = stability# R
A = A /\ S by A2, XBOOLE_1:28;
then A3: A is StableSet of (subrelstr S) by Th31;
consider As being StableSet of (subrelstr S) such that
A4: card As = stability# (subrelstr S) by Def6;
A5: card A <= card As by A3, A4, Def6;
stability# (subrelstr S) <= stability# R by Th44;
hence stability# (subrelstr S) = stability# R by A4, A1, A5, XXREAL_0:1; ::_thesis: verum
end;
begin
definition
let R be RelStr ;
let P be a_partition of the carrier of R;
attrP is Clique-wise means :Def11: :: DILWORTH:def 11
for x being set st x in P holds
x is Clique of R;
end;
:: deftheorem Def11 defines Clique-wise DILWORTH:def_11_:_
for R being RelStr
for P being a_partition of the carrier of R holds
( P is Clique-wise iff for x being set st x in P holds
x is Clique of R );
registration
let R be RelStr ;
cluster with_non-empty_elements Clique-wise for a_partition of the carrier of R;
existence
ex b1 being a_partition of the carrier of R st b1 is Clique-wise
proof
set cR = the carrier of R;
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is Clique-wise
then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
take S ; ::_thesis: S is Clique-wise
thus for x being set st x in S holds
x is Clique of R ; :: according to DILWORTH:def_11 ::_thesis: verum
end;
supposeA1: not R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is Clique-wise
take S = SmallestPartition the carrier of R; ::_thesis: S is Clique-wise
let z be set ; :: according to DILWORTH:def_11 ::_thesis: ( z in S implies z is Clique of R )
assume A2: z in S ; ::_thesis: z is Clique of R
S = { {x} where x is Element of the carrier of R : verum } by A1, EQREL_1:37;
then consider x being Element of the carrier of R such that
A3: z = {x} and
verum by A2;
thus z is Clique of R by A3, A1, SUBSET_1:33; ::_thesis: verum
end;
end;
end;
end;
definition
let R be RelStr ;
mode Clique-partition of R is Clique-wise a_partition of the carrier of R;
end;
registration
let R be empty RelStr ;
cluster empty -> Clique-wise for a_partition of the carrier of R;
coherence
for b1 being a_partition of the carrier of R st b1 is empty holds
b1 is Clique-wise
proof
let P be a_partition of the carrier of R; ::_thesis: ( P is empty implies P is Clique-wise )
assume P is empty ; ::_thesis: P is Clique-wise
let x be set ; :: according to DILWORTH:def_11 ::_thesis: ( x in P implies x is Clique of R )
thus ( x in P implies x is Clique of R ) ; ::_thesis: verum
end;
end;
theorem Th46: :: DILWORTH:46
for R being finite RelStr
for C being Clique-partition of R holds card C >= stability# R
proof
let R be finite RelStr ; ::_thesis: for C being Clique-partition of R holds card C >= stability# R
let C be Clique-partition of R; ::_thesis: card C >= stability# R
assume A1: card C < stability# R ; ::_thesis: contradiction
consider A being StableSet of R such that
A2: card A = stability# R by Def6;
( card (card C) = card C & card (card A) = card A ) ;
then A3: card C in card A by 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;
supposeA4: not R is empty ; ::_thesis: contradiction
defpred S1[ set , set ] means ( $1 in A & $2 in C & $1 in $2 );
A5: 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 A6: x in A ; ::_thesis: ex y being set st
( y in C & S1[x,y] )
reconsider x9 = x as Element of R by A6;
not the carrier of R is empty by A4;
then x9 in the carrier of R ;
then x in union C by EQREL_1:def_4;
then consider y being set such that
A7: x in y and
A8: y in C by TARSKI:def_4;
take y ; ::_thesis: ( y in C & S1[x,y] )
thus ( y in C & S1[x,y] ) by A6, A7, A8; ::_thesis: verum
end;
consider f being Function of A,C such that
A9: for x being set st x in A holds
S1[x,f . x] from FUNCT_2:sch_1(A5);
consider x, y being set such that
A10: x in A and
A11: y in A and
A12: x <> y and
A13: f . x = f . y by A4, A3, FINSEQ_4:65;
f . x in C by A10, FUNCT_2:5;
then A14: f . x is Clique of R by Def11;
( x in f . x & y in f . x ) by A13, A10, A11, A9;
hence contradiction by A14, A10, A11, A12, Th15; ::_thesis: verum
end;
end;
end;
theorem Th47: :: DILWORTH:47
for R being with_finite_stability# RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )
proof
let R be with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )
let A be StableSet of R; ::_thesis: for C being Clique-partition of R st card C = card A holds
ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )
let C be Clique-partition of R; ::_thesis: ( card C = card A implies ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) ) )
assume A1: card C = card A ; ::_thesis: ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )
set cR = the carrier of R;
percases ( R is empty or not R is empty ) ;
supposeA2: R is empty ; ::_thesis: ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )
then the carrier of R is empty ;
then A3: C = {} by EQREL_1:32;
set f = the Function of A,C;
dom the Function of A,C = {} by A2;
then reconsider f = {} as Function of A,C by RELAT_1:41;
A4: f is onto by A3, FUNCT_2:def_3, RELAT_1:38;
take f ; ::_thesis: ( f is bijective & ( for x being set st x in A holds
x in f . x ) )
thus f is bijective by A4; ::_thesis: for x being set st x in A holds
x in f . x
thus for x being set st x in A holds
x in f . x ; ::_thesis: verum
end;
supposeA5: not R is empty ; ::_thesis: ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )
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 x9 = x as Element of R ;
not the carrier of R is empty by A5;
then x9 in the carrier of R ;
then x9 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);
take f ; ::_thesis: ( f is bijective & ( for x being set st x in A holds
x in f . x ) )
A11: 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
A12: x1 in dom f and
A13: x2 in dom f and
A14: f . x1 = f . x2 ; ::_thesis: x1 = x2
A15: x1 in f . x1 by A12, A10;
A16: x2 in f . x2 by A13, A10;
f . x1 in C by A5, A12, FUNCT_2:5;
then f . x1 is Clique of R by Def11;
hence x1 = x2 by A12, A13, A15, A16, A14, Th15; ::_thesis: verum
end;
C is finite by A1;
then rng f = C by A1, A11, FINSEQ_4:63;
then f is onto by FUNCT_2:def_3;
hence f is bijective by A11; ::_thesis: for x being set st x in A holds
x in f . x
let x be set ; ::_thesis: ( x in A implies x in f . x )
assume x in A ; ::_thesis: x in f . x
hence x in f . x by A10; ::_thesis: verum
end;
end;
end;
theorem Th48: :: DILWORTH:48
for R being finite RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
proof
let R be finite RelStr ; ::_thesis: for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
let A be StableSet of R; ::_thesis: for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
let C be Clique-partition of R; ::_thesis: ( card C = card A implies for c being set st c in C holds
ex a being Element of A st c /\ A = {a} )
assume A1: card C = card A ; ::_thesis: for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
consider f being Function of A,C such that
A2: f is bijective and
A3: for x being set st x in A holds
x in f . x by A1, Th47;
let c be set ; ::_thesis: ( c in C implies ex a being Element of A st c /\ A = {a} )
assume A4: c in C ; ::_thesis: ex a being Element of A st c /\ A = {a}
rng f = C by A2, FUNCT_2:def_3;
then consider x being set such that
A5: x in dom f and
A6: c = f . x by A4, FUNCT_1:def_3;
A7: x in c by A5, A6, A3;
reconsider a = x as Element of A by A5;
take a ; ::_thesis: c /\ A = {a}
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_c_/\_A_implies_z_=_a_)_&_(_z_=_a_implies_z_in_c_/\_A_)_)
let z be set ; ::_thesis: ( ( z in c /\ A implies z = a ) & ( z = a implies z in c /\ A ) )
hereby ::_thesis: ( z = a implies z in c /\ A )
assume z in c /\ A ; ::_thesis: z = a
then A8: ( z in c & z in A ) by XBOOLE_0:def_4;
c is Clique of R by A4, Def11;
hence z = a by A8, A7, Th15; ::_thesis: verum
end;
assume z = a ; ::_thesis: z in c /\ A
hence z in c /\ A by A7, A5, XBOOLE_0:def_4; ::_thesis: verum
end;
hence c /\ A = {a} by TARSKI:def_1; ::_thesis: verum
end;
theorem Th49: :: DILWORTH:49
for R being non empty transitive antisymmetric with_finite_stability# RelStr
for A being StableSet of R
for U being Clique-partition of (subrelstr (Upper A))
for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
proof
let R be non empty transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R
for U being Clique-partition of (subrelstr (Upper A))
for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
let A be StableSet of R; ::_thesis: for U being Clique-partition of (subrelstr (Upper A))
for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
let U be Clique-partition of (subrelstr (Upper A)); ::_thesis: for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
let L be Clique-partition of (subrelstr (Lower A)); ::_thesis: ( card A = stability# R & card U = stability# R & card L = stability# R implies ex C being Clique-partition of R st card C = stability# R )
assume that
A1: card A = stability# R and
A2: card U = stability# R and
A3: card L = stability# R ; ::_thesis: ex C being Clique-partition of R st card C = stability# R
A4: not A is empty by A1;
set aA = Upper A;
set bA = Lower A;
set cR = the carrier of R;
set Pa = subrelstr (Upper A);
set Pb = subrelstr (Lower A);
A5: Upper A = the carrier of (subrelstr (Upper A)) by YELLOW_0:def_15;
A6: Lower A = the carrier of (subrelstr (Lower A)) by YELLOW_0:def_15;
reconsider Pa = subrelstr (Upper A) as non empty transitive antisymmetric with_finite_stability# RelStr by A4;
A /\ (Upper A) = A by XBOOLE_1:21;
then A is StableSet of Pa by Th31;
then consider f being Function of A,U such that
A7: f is bijective and
A8: for x being set st x in A holds
x in f . x by A1, A2, Th47;
A9: dom f = A by A4, FUNCT_2:def_1;
A10: rng f = U by A7, FUNCT_2:def_3;
reconsider Pb = subrelstr (Lower A) as non empty transitive antisymmetric with_finite_stability# RelStr by A4;
A /\ (Lower A) = A by XBOOLE_1:21;
then A is StableSet of Pb by Th31;
then consider g being Function of A,L such that
A11: g is bijective and
A12: for x being set st x in A holds
x in g . x by A1, A3, Th47;
A13: dom g = A by A4, FUNCT_2:def_1;
A14: rng g = L by A11, FUNCT_2:def_3;
set h = f .\/ g;
set C = rng (f .\/ g);
A15: dom (f .\/ g) = (dom f) \/ (dom g) by LEXBFS:def_2;
A16: rng (f .\/ g) c= bool the carrier of R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f .\/ g) or x in bool the carrier of R )
assume x in rng (f .\/ g) ; ::_thesis: x in bool the carrier of R
then consider a being set such that
A17: a in dom (f .\/ g) and
A18: (f .\/ g) . a = x by FUNCT_1:def_3;
A19: (f .\/ g) . a = (f . a) \/ (g . a) by A17, A15, LEXBFS:def_2;
f . a in U by A17, A15, FUNCT_2:5;
then A20: f . a c= the carrier of R by A5, XBOOLE_1:1;
g . a in L by A17, A15, FUNCT_2:5;
then g . a c= the carrier of R by A6, XBOOLE_1:1;
then x c= the carrier of R by A18, A19, A20, XBOOLE_1:8;
hence x in bool the carrier of R ; ::_thesis: verum
end;
A21: union (rng (f .\/ g)) = the carrier of R
proof
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_union_(rng_(f_.\/_g))_implies_x_in_the_carrier_of_R_)_&_(_x_in_[#]_R_implies_x_in_union_(rng_(f_.\/_g))_)_)
let x be set ; ::_thesis: ( ( x in union (rng (f .\/ g)) implies x in the carrier of R ) & ( x in [#] R implies b1 in union (rng (f .\/ g)) ) )
hereby ::_thesis: ( x in [#] R implies b1 in union (rng (f .\/ g)) )
assume x in union (rng (f .\/ g)) ; ::_thesis: x in the carrier of R
then consider Y being set such that
A22: x in Y and
A23: Y in rng (f .\/ g) by TARSKI:def_4;
consider a being set such that
A24: a in dom (f .\/ g) and
A25: Y = (f .\/ g) . a by A23, FUNCT_1:def_3;
A26: x in (f . a) \/ (g . a) by A24, A25, A22, A15, LEXBFS:def_2;
percases ( x in f . a or x in g . a ) by A26, XBOOLE_0:def_3;
supposeA27: x in f . a ; ::_thesis: x in the carrier of R
f . a in U by A24, A15, FUNCT_2:5;
then x in Upper A by A27, A5;
hence x in the carrier of R ; ::_thesis: verum
end;
supposeA28: x in g . a ; ::_thesis: x in the carrier of R
g . a in L by A24, A15, FUNCT_2:5;
then x in Lower A by A28, A6;
hence x in the carrier of R ; ::_thesis: verum
end;
end;
end;
assume x in [#] R ; ::_thesis: b1 in union (rng (f .\/ g))
then A29: x in (Upper A) \/ (Lower A) by A1, Th23;
percases ( x in Upper A or x in Lower A ) by A29, XBOOLE_0:def_3;
suppose x in Upper A ; ::_thesis: b1 in union (rng (f .\/ g))
then x in union U by A5, EQREL_1:def_4;
then consider Y being set such that
A30: x in Y and
A31: Y in U by TARSKI:def_4;
consider a being set such that
A32: a in dom f and
A33: Y = f . a by A31, A10, FUNCT_1:def_3;
A34: (f .\/ g) . a in rng (f .\/ g) by A32, A15, A9, A13, FUNCT_1:3;
(f .\/ g) . a = (f . a) \/ (g . a) by A32, A15, A9, A13, LEXBFS:def_2;
then x in (f .\/ g) . a by A30, A33, XBOOLE_0:def_3;
hence x in union (rng (f .\/ g)) by A34, TARSKI:def_4; ::_thesis: verum
end;
suppose x in Lower A ; ::_thesis: b1 in union (rng (f .\/ g))
then x in union L by A6, EQREL_1:def_4;
then consider Y being set such that
A35: x in Y and
A36: Y in L by TARSKI:def_4;
consider a being set such that
A37: a in dom g and
A38: Y = g . a by A36, A14, FUNCT_1:def_3;
A39: (f .\/ g) . a in rng (f .\/ g) by A37, A15, A9, A13, FUNCT_1:3;
(f .\/ g) . a = (f . a) \/ (g . a) by A37, A15, A9, A13, LEXBFS:def_2;
then x in (f .\/ g) . a by A35, A38, XBOOLE_0:def_3;
hence x in union (rng (f .\/ g)) by A39, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence union (rng (f .\/ g)) = the carrier of R by TARSKI:1; ::_thesis: verum
end;
A40: now__::_thesis:_for_a_being_Subset_of_the_carrier_of_R_st_a_in_rng_(f_.\/_g)_holds_
(_a_<>_{}_&_(_for_b_being_Subset_of_the_carrier_of_R_st_b_in_rng_(f_.\/_g)_&_a_<>_b_holds_
not_a_meets_b_)_)
let a be Subset of the carrier of R; ::_thesis: ( a in rng (f .\/ g) implies ( a <> {} & ( for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds
not a meets b ) ) )
assume a in rng (f .\/ g) ; ::_thesis: ( a <> {} & ( for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds
not a meets b ) )
then consider x being set such that
A41: x in dom (f .\/ g) and
A42: (f .\/ g) . x = a by FUNCT_1:def_3;
A43: (f .\/ g) . x = (f . x) \/ (g . x) by A41, A15, LEXBFS:def_2;
set cfx = f . x;
set cgx = g . x;
A44: f . x in U by A41, A15, FUNCT_2:5;
then reconsider cfx = f . x as Subset of Pa ;
A45: g . x in L by A41, A15, FUNCT_2:5;
then reconsider cgx = g . x as Subset of Pb ;
cfx <> {} by A44, EQREL_1:def_4;
hence a <> {} by A42, A43; ::_thesis: for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds
not a meets b
let b be Subset of the carrier of R; ::_thesis: ( b in rng (f .\/ g) & a <> b implies not a meets b )
assume b in rng (f .\/ g) ; ::_thesis: ( a <> b implies not a meets b )
then consider y being set such that
A46: y in dom (f .\/ g) and
A47: (f .\/ g) . y = b by FUNCT_1:def_3;
A48: (f .\/ g) . y = (f . y) \/ (g . y) by A46, A15, LEXBFS:def_2;
set cfy = f . y;
set cgy = g . y;
A49: f . y in U by A46, A15, FUNCT_2:5;
then reconsider cfy = f . y as Subset of Pa ;
A50: g . y in L by A46, A15, FUNCT_2:5;
then reconsider cgy = g . y as Subset of Pb ;
assume A51: a <> b ; ::_thesis: not a meets b
then A52: cfx <> cfy by A7, A42, A47, A41, A46, A15, A9, FUNCT_1:def_4;
A53: cgx <> cgy by A11, A51, A42, A47, A41, A46, A15, A13, FUNCT_1:def_4;
assume a meets b ; ::_thesis: contradiction
then a /\ b <> {} by XBOOLE_0:def_7;
then consider z being set such that
A54: z in a /\ b by XBOOLE_0:def_1;
A55: z in a by A54, XBOOLE_0:def_4;
A56: z in b by A54, XBOOLE_0:def_4;
set cfz = f . z;
set cgz = g . z;
percases ( ( z in cfx & z in cfy ) or ( z in cfx & z in cgy ) or ( z in cgx & z in cfy ) or ( z in cgx & z in cgy ) ) by A55, A56, A42, A47, A43, A48, XBOOLE_0:def_3;
suppose ( z in cfx & z in cfy ) ; ::_thesis: contradiction
then z in cfx /\ cfy by XBOOLE_0:def_4;
then cfx meets cfy by XBOOLE_0:def_7;
hence contradiction by A44, A49, A52, EQREL_1:def_4; ::_thesis: verum
end;
supposeA57: ( z in cfx & z in cgy ) ; ::_thesis: contradiction
then A58: z in A by A5, A6, Th22;
A59: z in f . z by A57, A5, A6, Th22, A8;
A60: f . z in U by A57, A5, A6, Th22, FUNCT_2:5;
then reconsider cfz = f . z as Subset of Pa ;
z in cfx /\ cfz by A57, A59, XBOOLE_0:def_4;
then cfz meets cfx by XBOOLE_0:def_7;
then cfz = cfx by A44, A60, EQREL_1:def_4;
then A61: z = x by A7, A41, A58, A15, A9, FUNCT_1:def_4;
A62: z in g . z by A57, A5, A6, Th22, A12;
A63: g . z in L by A57, A5, A6, Th22, FUNCT_2:5;
then reconsider cgz = g . z as Subset of Pb ;
z in cgz /\ cgy by A57, A62, XBOOLE_0:def_4;
then cgz meets cgy by XBOOLE_0:def_7;
then cgz = cgy by A50, A63, EQREL_1:def_4;
hence contradiction by A61, A51, A42, A47, A11, A46, A58, A15, A13, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA64: ( z in cgx & z in cfy ) ; ::_thesis: contradiction
then A65: z in A by A5, A6, Th22;
A66: z in f . z by A64, A5, A6, Th22, A8;
A67: f . z in U by A64, A5, A6, Th22, FUNCT_2:5;
then reconsider cfz = f . z as Subset of Pa ;
z in cfy /\ cfz by A64, A66, XBOOLE_0:def_4;
then cfz meets cfy by XBOOLE_0:def_7;
then cfz = cfy by A49, A67, EQREL_1:def_4;
then A68: z = y by A7, A46, A65, A15, A9, FUNCT_1:def_4;
A69: z in g . z by A64, A5, A6, Th22, A12;
A70: g . z in L by A64, A5, A6, Th22, FUNCT_2:5;
then reconsider cgz = g . z as Subset of Pb ;
z in cgz /\ cgx by A64, A69, XBOOLE_0:def_4;
then cgz meets cgx by XBOOLE_0:def_7;
then cgz = cgx by A45, A70, EQREL_1:def_4;
hence contradiction by A68, A51, A42, A47, A11, A41, A65, A15, A13, FUNCT_1:def_4; ::_thesis: verum
end;
suppose ( z in cgx & z in cgy ) ; ::_thesis: contradiction
then z in cgx /\ cgy by XBOOLE_0:def_4;
then cgx meets cgy by XBOOLE_0:def_7;
hence contradiction by A45, A50, A53, EQREL_1:def_4; ::_thesis: verum
end;
end;
end;
A71: for x being set st x in rng (f .\/ g) holds
x is Clique of R
proof
let c be set ; ::_thesis: ( c in rng (f .\/ g) implies c is Clique of R )
assume c in rng (f .\/ g) ; ::_thesis: c is Clique of R
then consider x being set such that
A72: x in dom (f .\/ g) and
A73: c = (f .\/ g) . x by FUNCT_1:def_3;
A74: c = (f . x) \/ (g . x) by A72, A73, A15, LEXBFS:def_2;
set cf = f . x;
set cg = g . x;
f . x in U by A72, A15, FUNCT_2:5;
then A75: f . x is Clique of Pa by Def11;
then A76: f . x is Clique of R by Th28;
g . x in L by A72, A15, FUNCT_2:5;
then A77: g . x is Clique of Pb by Def11;
then A78: g . x is Clique of R by Th28;
then reconsider c9 = c as Subset of R by A74, A76, XBOOLE_1:8;
now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_c9_&_b_in_c9_&_a_<>_b_&_not_a_<=_b_holds_
b_<=_a
let a, b be Element of R; ::_thesis: ( a in c9 & b in c9 & a <> b & not b1 <= b2 implies b2 <= b1 )
assume that
A79: a in c9 and
A80: b in c9 and
A81: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
A82: x in f . x by A72, A15, A8;
A83: x in g . x by A72, A15, A12;
reconsider x = x as Element of R by A72, A15, A9, A13;
percases ( ( a in f . x & b in f . x ) or ( a in f . x & b in g . x ) or ( a in g . x & b in f . x ) or ( a in g . x & b in g . x ) ) by A79, A80, A74, XBOOLE_0:def_3;
suppose ( a in f . x & b in f . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A76, A81, Th6; ::_thesis: verum
end;
supposeA84: ( a in f . x & b in g . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then A85: ( x = a or x <= a ) by A82, A72, A15, A75, Th35;
( x = b or b <= x ) by A83, A84, A72, A15, A77, Th34;
hence ( a <= b or b <= a ) by A81, A85, YELLOW_0:def_2; ::_thesis: verum
end;
supposeA86: ( a in g . x & b in f . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
then A87: ( x = a or a <= x ) by A83, A72, A15, A77, Th34;
( x = b or x <= b ) by A82, A86, A72, A15, A75, Th35;
hence ( a <= b or b <= a ) by A81, A87, YELLOW_0:def_2; ::_thesis: verum
end;
suppose ( a in g . x & b in g . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 )
hence ( a <= b or b <= a ) by A78, A81, Th6; ::_thesis: verum
end;
end;
end;
hence c is Clique of R by Th6; ::_thesis: verum
end;
A88: f .\/ g is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (f .\/ g) or not x2 in dom (f .\/ g) or not (f .\/ g) . x1 = (f .\/ g) . x2 or x1 = x2 )
assume that
A89: x1 in dom (f .\/ g) and
A90: x2 in dom (f .\/ g) and
A91: (f .\/ g) . x1 = (f .\/ g) . x2 ; ::_thesis: x1 = x2
A92: (f .\/ g) . x1 is Clique of R by A71, A89, FUNCT_1:3;
A93: (f .\/ g) . x1 = (f . x1) \/ (g . x1) by A15, A89, LEXBFS:def_2;
( x1 in f . x1 & x1 in g . x1 ) by A89, A15, A8, A12;
then A94: x1 in (f .\/ g) . x1 by A93, XBOOLE_0:def_3;
A95: (f .\/ g) . x2 = (f . x2) \/ (g . x2) by A15, A90, LEXBFS:def_2;
( x2 in f . x2 & x2 in g . x2 ) by A90, A15, A8, A12;
then x2 in (f .\/ g) . x2 by A95, XBOOLE_0:def_3;
hence x1 = x2 by A15, A89, A90, A91, A92, A94, Th15; ::_thesis: verum
end;
reconsider C = rng (f .\/ g) as Clique-partition of R by A16, A21, A40, A71, Def11, EQREL_1:def_4;
take C ; ::_thesis: card C = stability# R
card C = card (f .\/ g) by A88, PRE_POLY:19
.= card A by A15, A9, A13, CARD_1:62 ;
hence card C = stability# R by A1; ::_thesis: verum
end;
definition
let R be RelStr ;
let P be a_partition of the carrier of R;
attrP is StableSet-wise means :Def12: :: DILWORTH:def 12
for x being set st x in P holds
x is StableSet of R;
end;
:: deftheorem Def12 defines StableSet-wise DILWORTH:def_12_:_
for R being RelStr
for P being a_partition of the carrier of R holds
( P is StableSet-wise iff for x being set st x in P holds
x is StableSet of R );
registration
let R be RelStr ;
cluster with_non-empty_elements StableSet-wise for a_partition of the carrier of R;
existence
ex b1 being a_partition of the carrier of R st b1 is StableSet-wise
proof
set cR = the carrier of R;
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is StableSet-wise
then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
take S ; ::_thesis: S is StableSet-wise
let x be set ; :: according to DILWORTH:def_12 ::_thesis: ( x in S implies x is StableSet of R )
thus ( x in S implies x is StableSet of R ) ; ::_thesis: verum
end;
supposeA1: not R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is StableSet-wise
then reconsider RR = R as non empty RelStr ;
take S = SmallestPartition the carrier of R; ::_thesis: S is StableSet-wise
let z be set ; :: according to DILWORTH:def_12 ::_thesis: ( z in S implies z is StableSet of R )
assume A2: z in S ; ::_thesis: z is StableSet of R
S = { {x} where x is Element of the carrier of R : verum } by A1, EQREL_1:37;
then consider x being Element of RR such that
A3: z = {x} by A2;
thus z is StableSet of R by A3; ::_thesis: verum
end;
end;
end;
end;
definition
let R be RelStr ;
mode Coloring of R is StableSet-wise a_partition of the carrier of R;
end;
registration
let R be empty RelStr ;
cluster -> StableSet-wise for a_partition of the carrier of R;
coherence
for b1 being a_partition of the carrier of R holds b1 is StableSet-wise
proof
let P be a_partition of the carrier of R; ::_thesis: P is StableSet-wise
let x be set ; :: according to DILWORTH:def_12 ::_thesis: ( x in P implies x is StableSet of R )
thus ( x in P implies x is StableSet of R ) ; ::_thesis: verum
end;
end;
theorem :: DILWORTH:50
for R being finite RelStr
for C being Coloring of R holds card C >= clique# R
proof
let R be finite RelStr ; ::_thesis: for C being Coloring of R holds card C >= clique# R
let C be Coloring of R; ::_thesis: card C >= clique# R
assume A1: card C < clique# R ; ::_thesis: contradiction
consider A being Clique of R such that
A2: card A = clique# R by Def4;
( card (card C) = card C & card (card A) = card A ) ;
then A3: card C in card A by 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;
supposeA4: not R is empty ; ::_thesis: contradiction
defpred S1[ set , set ] means ( $1 in A & $2 in C & $1 in $2 );
A5: 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 A6: x in A ; ::_thesis: ex y being set st
( y in C & S1[x,y] )
reconsider x9 = x as Element of R by A6;
not the carrier of R is empty by A4;
then x9 in the carrier of R ;
then x in union C by EQREL_1:def_4;
then consider y being set such that
A7: x in y and
A8: y in C by TARSKI:def_4;
take y ; ::_thesis: ( y in C & S1[x,y] )
thus ( y in C & S1[x,y] ) by A6, A7, A8; ::_thesis: verum
end;
consider f being Function of A,C such that
A9: for x being set st x in A holds
S1[x,f . x] from FUNCT_2:sch_1(A5);
consider x, y being set such that
A10: x in A and
A11: y in A and
A12: x <> y and
A13: f . x = f . y by A4, A3, FINSEQ_4:65;
f . x in C by A10, FUNCT_2:5;
then A14: f . x is StableSet of R by Def12;
( x in f . x & y in f . x ) by A13, A10, A11, A9;
hence contradiction by A14, A10, A11, A12, Th15; ::_thesis: verum
end;
end;
end;
begin
theorem Th51: :: DILWORTH:51
for R being finite transitive antisymmetric RelStr ex C being Clique-partition of R st card C = stability# R
proof
defpred S1[ Nat] means for P being finite transitive antisymmetric RelStr st card P = $1 holds
ex C being Clique-partition of P st card C = stability# P;
A1: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A2: for k being Nat st k < n holds
S1[k] ; ::_thesis: S1[n]
let P be finite transitive antisymmetric RelStr ; ::_thesis: ( card P = n implies ex C being Clique-partition of P st card C = stability# P )
assume A3: card P = n ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
set wP = stability# P;
percases ( n = 0 or n > 0 ) ;
supposeA4: n = 0 ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
then P is empty by A3;
then reconsider C = {} as Clique-partition of P by EQREL_1:45;
take C ; ::_thesis: card C = stability# P
P is empty by A3, A4;
hence card C = stability# P by A3, A4; ::_thesis: verum
end;
supposeA5: n > 0 ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
percases ( ex A being StableSet of P st
( card A = stability# P & A <> minimals P & A <> maximals P ) or for A being StableSet of P holds
( not card A = stability# P or A = minimals P or A = maximals P ) ) ;
suppose ex A being StableSet of P st
( card A = stability# P & A <> minimals P & A <> maximals P ) ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
then consider A being StableSet of P such that
A6: card A = stability# P and
A7: A <> minimals P and
A8: A <> maximals P ;
set aA = Upper A;
set bA = Lower A;
set cP = the carrier of P;
set Pa = subrelstr (Upper A);
set Pb = subrelstr (Lower A);
reconsider PP = P as non empty finite transitive antisymmetric RelStr by A5, A3;
A9: Upper A = the carrier of (subrelstr (Upper A)) by YELLOW_0:def_15;
A10: Lower A = the carrier of (subrelstr (Lower A)) by YELLOW_0:def_15;
not minimals PP c= Upper A by A7, Th40, Th26;
then consider mi being set such that
A11: mi in minimals P and
A12: not mi in Upper A by TARSKI:def_3;
not maximals PP c= Lower A by A8, Th41, Th27;
then consider ma being set such that
A13: ma in maximals P and
A14: not ma in Lower A by TARSKI:def_3;
reconsider Pa = subrelstr (Upper A) as finite transitive antisymmetric RelStr ;
mi in the carrier of P by A11;
then Upper A c< the carrier of P by A12, XBOOLE_0:def_8;
then card Pa < card P by A9, CARD_2:48;
then consider Ca being Clique-partition of Pa such that
A15: card Ca = stability# Pa by A2, A3;
A16: stability# Pa = stability# P by A6, Th45, XBOOLE_1:7;
reconsider Pb = subrelstr (Lower A) as finite transitive antisymmetric RelStr ;
ma in the carrier of P by A13;
then Lower A c< the carrier of P by A14, XBOOLE_0:def_8;
then card Pb < card P by A10, CARD_2:48;
then consider L being Clique-partition of Pb such that
A17: card L = stability# Pb by A2, A3;
stability# Pb = stability# P by A6, Th45, XBOOLE_1:7;
then consider C being Clique-partition of P such that
A18: card C = stability# PP by A6, A15, A16, A17, Th49;
take C ; ::_thesis: card C = stability# P
thus card C = stability# P by A18; ::_thesis: verum
end;
supposeA19: for A being StableSet of P holds
( not card A = stability# P or A = minimals P or A = maximals P ) ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
consider S being StableSet of P such that
A20: card S = stability# P by Def6;
reconsider PP = P as non empty finite transitive antisymmetric RelStr by A5, A3;
set cR = the carrier of PP;
set a = the Element of minimals P;
A21: the Element of minimals P in minimals PP ;
then reconsider a = the Element of minimals P as Element of PP ;
consider b being Element of PP such that
A22: b is_maximal_in [#] PP and
A23: ( a = b or a < b ) by Th38;
A24: b in maximals P by A22, Def10;
set cP = the carrier of P;
set Cn = {a,b};
set cP9 = the carrier of P \ {a,b};
A25: the carrier of P = ( the carrier of P \ {a,b}) \/ {a,b} by XBOOLE_1:45;
A26: the carrier of P \ {a,b} misses {a,b} by XBOOLE_1:79;
then A27: the carrier of P \ ( the carrier of P \ {a,b}) = {a,b} by A25, XBOOLE_1:88;
reconsider cP9 = the carrier of P \ {a,b} as Subset of the carrier of PP ;
set P9 = subrelstr cP9;
A28: cP9 = the carrier of (subrelstr cP9) by YELLOW_0:def_15;
A29: card cP9 = card (subrelstr cP9) by YELLOW_0:def_15;
card cP9 = (card the carrier of P) - (card {a,b}) by CARD_2:44;
then consider C being Clique-partition of (subrelstr cP9) such that
A30: card C = stability# (subrelstr cP9) by A2, A3, A29, XREAL_1:44;
A31: not {a,b} in C
proof
assume A32: {a,b} in C ; ::_thesis: contradiction
a in {a,b} by TARSKI:def_2;
hence contradiction by A26, A28, A32, ZFMISC_1:49; ::_thesis: verum
end;
set wP = stability# PP;
set wP1 = (stability# PP) - 1;
0 + 1 <= stability# PP by NAT_1:13;
then (0 + 1) - 1 <= (stability# PP) - 1 by XREAL_1:9;
then (stability# PP) - 1 in NAT by INT_1:3;
then reconsider wP1 = (stability# PP) - 1 as Nat ;
set S9 = S /\ cP9;
S /\ the carrier of P = S by XBOOLE_1:28;
then A33: S /\ cP9 = S \ {a,b} by XBOOLE_1:49;
A34: {a,b} = {a} \/ {b} by ENUMSET1:1;
reconsider S9 = S /\ cP9 as StableSet of (subrelstr cP9) by Th31;
A35: card S9 = wP1
proof
percases ( S = minimals P or S = maximals PP ) by A19, A20;
supposeA36: S = minimals P ; ::_thesis: card S9 = wP1
S9 = S \ {a}
proof
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: S9 = S \ {a}
hence S9 = S \ {a} by A33, ENUMSET1:29; ::_thesis: verum
end;
supposeA37: a <> b ; ::_thesis: S9 = S \ {a}
now__::_thesis:_not_b_in_minimals_PP
assume b in minimals PP ; ::_thesis: contradiction
then b is_minimal_in [#] PP by Def9;
hence contradiction by A37, A23, WAYBEL_4:56; ::_thesis: verum
end;
hence S9 = S \ {a} by A33, A34, A36, Th1; ::_thesis: verum
end;
end;
end;
hence card S9 = (card S) - (card {a}) by A36, EULER_1:4
.= wP1 by A20, CARD_1:30 ;
::_thesis: verum
end;
supposeA38: S = maximals PP ; ::_thesis: card S9 = wP1
A39: S9 = S \ {b}
proof
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: S9 = S \ {b}
hence S9 = S \ {b} by A33, ENUMSET1:29; ::_thesis: verum
end;
supposeA40: a <> b ; ::_thesis: S9 = S \ {b}
now__::_thesis:_not_a_in_maximals_PP
assume a in maximals PP ; ::_thesis: contradiction
then a is_maximal_in [#] PP by Def10;
hence contradiction by A40, A23, WAYBEL_4:55; ::_thesis: verum
end;
hence S9 = S \ {b} by A33, A34, A38, Th1; ::_thesis: verum
end;
end;
end;
b in S by A38, A22, Def10;
hence card S9 = (card S) - (card {b}) by A39, EULER_1:4
.= wP1 by A20, CARD_1:30 ;
::_thesis: verum
end;
end;
end;
for T being StableSet of (subrelstr cP9) holds card T <= card S9
proof
let T be StableSet of (subrelstr cP9); ::_thesis: card T <= card S9
assume card T > card S9 ; ::_thesis: contradiction
then card T >= (card S9) + 1 by NAT_1:13;
then consider V being StableSet of (subrelstr cP9) such that
A41: card V = (card S9) + 1 by Th17;
V is StableSet of P by Th30;
then ( V = minimals P or V = maximals P ) by A19, A41, A35;
hence contradiction by A21, A24, A28, A26, ZFMISC_1:49; ::_thesis: verum
end;
then A42: (stability# (subrelstr cP9)) + 1 = ((stability# PP) - 1) + 1 by A35, Def6
.= stability# PP ;
set CC = C \/ {{a,b}};
cP9 <> the carrier of P by A27, XBOOLE_1:37;
then A43: cP9 c< the carrier of P by XBOOLE_0:def_8;
now__::_thesis:_for_x_being_set_st_x_in_C_\/_{{a,b}}_holds_
x_is_Clique_of_P
let x be set ; ::_thesis: ( x in C \/ {{a,b}} implies b1 is Clique of P )
assume A44: x in C \/ {{a,b}} ; ::_thesis: b1 is Clique of P
percases ( x in C or x in {{a,b}} ) by A44, XBOOLE_0:def_3;
suppose x in C ; ::_thesis: b1 is Clique of P
then x is Clique of (subrelstr cP9) by Def11;
hence x is Clique of P by Th28; ::_thesis: verum
end;
suppose x in {{a,b}} ; ::_thesis: b1 is Clique of P
then A45: x = {a,b} by TARSKI:def_1;
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: b1 is Clique of P
then x = {a} by A45, ENUMSET1:29;
hence x is Clique of P ; ::_thesis: verum
end;
suppose a <> b ; ::_thesis: b1 is Clique of P
then a <= b by A23, ORDERS_2:def_6;
hence x is Clique of P by A45, Th8; ::_thesis: verum
end;
end;
end;
end;
end;
then reconsider CC = C \/ {{a,b}} as Clique-partition of P by A27, A28, Th4, Def11, A43;
take CC ; ::_thesis: card CC = stability# P
thus card CC = stability# P by A30, A42, A31, CARD_2:41; ::_thesis: verum
end;
end;
end;
end;
end;
A46: for n being Nat holds S1[n] from NAT_1:sch_4(A1);
let R be finite transitive antisymmetric RelStr ; ::_thesis: ex C being Clique-partition of R st card C = stability# R
card R = card R ;
hence ex C being Clique-partition of R st card C = stability# R by A46; ::_thesis: verum
end;
definition
let R be non empty with_finite_stability# RelStr ;
let C be Subset of R;
attrC is strong-chain means :Def13: :: DILWORTH:def 13
for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) );
end;
:: deftheorem Def13 defines strong-chain DILWORTH:def_13_:_
for R being non empty with_finite_stability# RelStr
for C being Subset of R holds
( C is strong-chain iff for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) ) );
registration
let R be non empty with_finite_stability# RelStr ;
cluster strong-chain -> clique for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is strong-chain holds
b1 is clique
proof
let C be Subset of R; ::_thesis: ( C is strong-chain implies C is clique )
assume A1: C is strong-chain ; ::_thesis: C is clique
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 )
set S = {a,b};
reconsider S = {a,b} as non empty finite Subset of R ;
consider P being Clique-partition of (subrelstr S) such that
card P <= stability# R and
A5: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) by A1, Def13;
consider c being set such that
A6: c in P and
A7: S /\ C c= c and
for d being set st d in P & d <> c holds
C /\ d = {} by A5;
c is Clique of (subrelstr S) by A6, Def11;
then A8: c is Clique of R by Th28;
( a in S & b in S ) by TARSKI:def_2;
then ( a in S /\ C & b in S /\ C ) by A2, A3, XBOOLE_0:def_4;
hence ( a <= b or b <= a ) by A7, A8, A4, Th6; ::_thesis: verum
end;
hence C is clique by Th6; ::_thesis: verum
end;
end;
registration
let R be non empty transitive antisymmetric with_finite_stability# RelStr ;
cluster1 -element -> strong-chain for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is 1 -element holds
b1 is strong-chain
proof
let C be Subset of R; ::_thesis: ( C is 1 -element implies C is strong-chain )
assume C is 1 -element ; ::_thesis: C is strong-chain
then consider x being set such that
A1: C = {x} by ZFMISC_1:131;
let S be non empty finite Subset of R; :: according to DILWORTH:def_13 ::_thesis: ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) )
consider P being Clique-partition of (subrelstr S) such that
A2: card P = stability# (subrelstr S) by Th51;
A3: S = the carrier of (subrelstr S) by YELLOW_0:def_15;
take P ; ::_thesis: ( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) )
thus card P <= stability# R by A2, Th44; ::_thesis: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
percases ( x in S or not x in S ) ;
suppose x in S ; ::_thesis: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
then x in union P by A3, EQREL_1:def_4;
then consider c being set such that
A4: x in c and
A5: c in P by TARSKI:def_4;
take c ; ::_thesis: ( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
thus c in P by A5; ::_thesis: ( S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
thus S /\ C c= c ::_thesis: for d being set st d in P & d <> c holds
C /\ d = {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S /\ C or a in c )
assume a in S /\ C ; ::_thesis: a in c
then a in C by XBOOLE_0:def_4;
hence a in c by A4, A1, TARSKI:def_1; ::_thesis: verum
end;
let d be set ; ::_thesis: ( d in P & d <> c implies C /\ d = {} )
assume that
A6: d in P and
A7: d <> c ; ::_thesis: C /\ d = {}
assume C /\ d <> {} ; ::_thesis: contradiction
then consider a being set such that
A8: a in C /\ d by XBOOLE_0:def_1;
reconsider d = d, c = c as Subset of S by A6, A5, YELLOW_0:def_15;
a in C by A8, XBOOLE_0:def_4;
then a = x by A1, TARSKI:def_1;
then x in d by A8, XBOOLE_0:def_4;
then x in d /\ c by A4, XBOOLE_0:def_4;
then d meets c by XBOOLE_0:def_7;
hence contradiction by A6, A5, A7, EQREL_1:def_4; ::_thesis: verum
end;
supposeA9: not x in S ; ::_thesis: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) )
set c = the Element of P;
take the Element of P ; ::_thesis: ( the Element of P in P & S /\ C c= the Element of P & ( for d being set st d in P & d <> the Element of P holds
C /\ d = {} ) )
thus the Element of P in P ; ::_thesis: ( S /\ C c= the Element of P & ( for d being set st d in P & d <> the Element of P holds
C /\ d = {} ) )
C misses S by A9, A1, ZFMISC_1:50;
then S /\ C = {} by XBOOLE_0:def_7;
hence S /\ C c= the Element of P by XBOOLE_1:2; ::_thesis: for d being set st d in P & d <> the Element of P holds
C /\ d = {}
let d be set ; ::_thesis: ( d in P & d <> the Element of P implies C /\ d = {} )
assume that
A10: d in P and
d <> the Element of P ; ::_thesis: C /\ d = {}
not x in d by A9, A3, A10;
then C misses d by A1, ZFMISC_1:50;
hence C /\ d = {} by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
end;
theorem Th52: :: DILWORTH:52
for R being non empty transitive antisymmetric with_finite_stability# RelStr ex S being non empty Subset of R st
( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
proof
let R be non empty transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: ex S being non empty Subset of R st
( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
set E = { C where C is Subset of R : C is strong-chain } ;
set x = the Element of R;
A1: { the Element of R} in { C where C is Subset of R : C is strong-chain } ;
now__::_thesis:_for_Z_being_set_st_Z_c=__{__C_where_C_is_Subset_of_R_:_C_is_strong-chain__}__&_Z_is_c=-linear_holds_
ex_Y_being_set_st_
(_Y_in__{__C_where_C_is_Subset_of_R_:_C_is_strong-chain__}__&_(_for_X1_being_set_st_X1_in_Z_holds_
X1_c=_Y_)_)
let Z be set ; ::_thesis: ( Z c= { C where C is Subset of R : C is strong-chain } & Z is c=-linear implies ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A2: Z c= { C where C is Subset of R : C is strong-chain } and
A3: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
set Y = union Z;
take Y = union Z; ::_thesis: ( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
now__::_thesis:_for_B_being_set_st_B_in_Z_holds_
B_c=_the_carrier_of_R
let B be set ; ::_thesis: ( B in Z implies B c= the carrier of R )
assume B in Z ; ::_thesis: B c= the carrier of R
then B in { C where C is Subset of R : C is strong-chain } by A2;
then ex C being Subset of R st
( C = B & C is strong-chain ) ;
hence B c= the carrier of R ; ::_thesis: verum
end;
then reconsider Y9 = Y as Subset of R by ZFMISC_1:76;
Y9 is strong-chain
proof
let S be non empty finite Subset of R; :: according to DILWORTH:def_13 ::_thesis: ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )
set F = S /\ Y;
percases ( S /\ Y is empty or not S /\ Y is empty ) ;
supposeA4: S /\ Y is empty ; ::_thesis: ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )
consider p being Clique-partition of (subrelstr S) such that
A5: card p = stability# (subrelstr S) by Th51;
take p ; ::_thesis: ( card p <= stability# R & ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) ) )
thus card p <= stability# R by Th44, A5; ::_thesis: ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
set c = the Element of p;
take the Element of p ; ::_thesis: ( the Element of p in p & S /\ Y9 c= the Element of p & ( for d being set st d in p & d <> the Element of p holds
Y9 /\ d = {} ) )
thus the Element of p in p ; ::_thesis: ( S /\ Y9 c= the Element of p & ( for d being set st d in p & d <> the Element of p holds
Y9 /\ d = {} ) )
thus S /\ Y9 c= the Element of p by A4, XBOOLE_1:2; ::_thesis: for d being set st d in p & d <> the Element of p holds
Y9 /\ d = {}
let d be set ; ::_thesis: ( d in p & d <> the Element of p implies Y9 /\ d = {} )
assume that
A6: d in p and
d <> the Element of p ; ::_thesis: Y9 /\ d = {}
d c= the carrier of (subrelstr S) by A6;
then d c= S by YELLOW_0:def_15;
hence Y9 /\ d = {} by A4, XBOOLE_1:3, XBOOLE_1:26; ::_thesis: verum
end;
supposeA7: not S /\ Y is empty ; ::_thesis: ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds
Y9 /\ d = {} ) ) )
then A8: not Z is empty by ZFMISC_1:2;
defpred S1[ set , set ] means ( $1 in S /\ Y & $2 in Z & $1 in $2 );
A9: for x being set st x in S /\ Y holds
ex y being set st
( y in Z & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in S /\ Y implies ex y being set st
( y in Z & S1[x,y] ) )
assume A10: x in S /\ Y ; ::_thesis: ex y being set st
( y in Z & S1[x,y] )
then x in Y by XBOOLE_0:def_4;
then consider y being set such that
A11: x in y and
A12: y in Z by TARSKI:def_4;
take y ; ::_thesis: ( y in Z & S1[x,y] )
thus ( y in Z & S1[x,y] ) by A12, A10, A11; ::_thesis: verum
end;
consider f being Function of (S /\ Y),Z such that
A13: for x being set st x in S /\ Y holds
S1[x,f . x] from FUNCT_2:sch_1(A9);
set rf = rng f;
( rng f c= Z & Z is c=-linear implies rng f is c=-linear ) ;
then consider m being set such that
A14: m in rng f and
A15: for C being set st C in rng f holds
C c= m by A3, A7, A8, FINSET_1:12, RELAT_1:def_19;
rng f c= Z by RELAT_1:def_19;
then m in Z by A14;
then m in { C where C is Subset of R : C is strong-chain } by A2;
then consider C being Subset of R such that
A16: m = C and
A17: C is strong-chain ;
A18: S /\ Y c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ Y or x in C )
assume A19: x in S /\ Y ; ::_thesis: x in C
then A20: x in f . x by A13;
f . x c= C by A16, A15, A19, A8, FUNCT_2:4;
hence x in C by A20; ::_thesis: verum
end;
consider p being Clique-partition of (subrelstr S) such that
A21: card p <= stability# R and
A22: ex c being set st
( c in p & S /\ C c= c & ( for d being set st d in p & d <> c holds
C /\ d = {} ) ) by A17, Def13;
take p ; ::_thesis: ( card p <= stability# R & ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) ) )
thus card p <= stability# R by A21; ::_thesis: ex c being set st
( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
consider c being set such that
A23: c in p and
A24: S /\ C c= c and
A25: for d being set st d in p & d <> c holds
C /\ d = {} by A22;
take c ; ::_thesis: ( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
thus c in p by A23; ::_thesis: ( S /\ Y9 c= c & ( for d being set st d in p & d <> c holds
Y9 /\ d = {} ) )
thus S /\ Y9 c= c ::_thesis: for d being set st d in p & d <> c holds
Y9 /\ d = {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ Y9 or x in c )
assume x in S /\ Y9 ; ::_thesis: x in c
then ( x in S & x in C ) by A18, XBOOLE_0:def_4;
then x in S /\ C by XBOOLE_0:def_4;
hence x in c by A24; ::_thesis: verum
end;
let d be set ; ::_thesis: ( d in p & d <> c implies Y9 /\ d = {} )
assume that
A26: d in p and
A27: d <> c ; ::_thesis: Y9 /\ d = {}
assume Y9 /\ d <> {} ; ::_thesis: contradiction
then consider x being set such that
A28: x in Y9 /\ d by XBOOLE_0:def_1;
A29: x in Y9 by A28, XBOOLE_0:def_4;
A30: x in d by A28, XBOOLE_0:def_4;
d is Subset of S by A26, YELLOW_0:def_15;
then x in S /\ Y by A30, A29, XBOOLE_0:def_4;
then x in C /\ d by A30, A18, XBOOLE_0:def_4;
hence contradiction by A26, A27, A25; ::_thesis: verum
end;
end;
end;
hence Y in { C where C is Subset of R : C is strong-chain } ; ::_thesis: for X1 being set st X1 in Z holds
X1 c= Y
let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= Y )
assume A31: X1 in Z ; ::_thesis: X1 c= Y
thus X1 c= Y by A31, ZFMISC_1:74; ::_thesis: verum
end;
then consider Y being set such that
A32: Y in { C where C is Subset of R : C is strong-chain } and
A33: for Z being set st Z in { C where C is Subset of R : C is strong-chain } & Z <> Y holds
not Y c= Z by A1, ORDERS_1:65;
consider C being Subset of R such that
A34: Y = C and
A35: C is strong-chain by A32;
reconsider S = C as non empty Subset of R by A34, A1, A33, XBOOLE_1:2;
take S ; ::_thesis: ( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
thus S is strong-chain by A35; ::_thesis: for D being Subset of R holds
( not D is strong-chain or not S c< D )
let D be Subset of R; ::_thesis: ( not D is strong-chain or not S c< D )
assume that
A36: D is strong-chain and
A37: S c< D ; ::_thesis: contradiction
A38: D in { C where C is Subset of R : C is strong-chain } by A36;
( D <> S & S c= D ) by A37, XBOOLE_0:def_8;
hence contradiction by A34, A38, A33; ::_thesis: verum
end;
theorem :: DILWORTH:53
for R being transitive antisymmetric with_finite_stability# RelStr ex C being Clique-partition of R st card C = stability# R
proof
let R be transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: ex C being Clique-partition of R st card C = stability# R
percases ( R is finite or R is infinite ) ;
suppose R is finite ; ::_thesis: ex C being Clique-partition of R st card C = stability# R
hence ex C being Clique-partition of R st card C = stability# R by Th51; ::_thesis: verum
end;
supposeA1: R is infinite ; ::_thesis: ex C being Clique-partition of R st card C = stability# R
defpred S1[ Nat] means for P being non empty transitive antisymmetric with_finite_stability# RelStr st stability# P = $1 holds
ex C being Clique-partition of P st card C = stability# P;
A2: S1[ 0 ] ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let P be non empty transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: ( stability# P = k + 1 implies ex C being Clique-partition of P st card C = stability# P )
assume A5: stability# P = k + 1 ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
consider C being non empty Subset of P such that
A6: C is strong-chain and
A7: for D being Subset of P holds
( not D is strong-chain or not C c< D ) by Th52;
set cP = the carrier of P;
percases ( C = the carrier of P or C <> the carrier of P ) ;
supposeA8: C = the carrier of P ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
for x being set st x in {C} holds
x is Clique of P by A6, TARSKI:def_1;
then reconsider Cp = {C} as Clique-partition of P by Def11, A8, EQREL_1:39;
take Cp ; ::_thesis: card Cp = stability# P
A9: the carrier of P = [#] P ;
thus card Cp = 1 by CARD_1:30
.= stability# P by A9, A6, A8, Th20 ; ::_thesis: verum
end;
suppose C <> the carrier of P ; ::_thesis: ex C being Clique-partition of P st card C = stability# P
then A10: C c< the carrier of P by XBOOLE_0:def_8;
set cP9 = the carrier of P \ C;
A11: the carrier of P \ ( the carrier of P \ C) = the carrier of P /\ C by XBOOLE_1:48
.= C by XBOOLE_1:28 ;
reconsider cP9 = the carrier of P \ C as Subset of P ;
cP9 <> {} by A10, XBOOLE_1:105;
then reconsider P9 = subrelstr cP9 as non empty transitive antisymmetric with_finite_stability# RelStr ;
A12: cP9 = the carrier of P9 by YELLOW_0:def_15;
A13: stability# P9 <= k + 1 by A5, Th44;
A14: stability# P9 <> k + 1
proof
assume A15: stability# P9 = k + 1 ; ::_thesis: contradiction
consider A being finite StableSet of P9 such that
A16: card A = stability# P9 by Def6;
reconsider A9 = A as non empty finite StableSet of P by A16, Th30;
defpred S2[ set , set , set ] means for c being set holds
( not c in $2 or not $1 /\ $3 c= c or ex d being set st
( d in $2 & d <> c & $3 /\ d <> {} ) );
defpred S3[ finite Subset of P, set ] means for p being Clique-partition of (subrelstr $1) st card p <= stability# P holds
S2[$1,p,$2];
defpred S4[ set , set ] means ex S being non empty finite Subset of P st
( $2 = S & $1 in $2 & S3[S,C \/ {$1}] );
A17: for x being set st x in A holds
ex y being set st S4[x,y]
proof
let a be set ; ::_thesis: ( a in A implies ex y being set st S4[a,y] )
assume A18: a in A ; ::_thesis: ex y being set st S4[a,y]
A c= the carrier of P by A12, XBOOLE_1:1;
then {a} c= the carrier of P by A18, ZFMISC_1:31;
then reconsider Ca = C \/ {a} as Subset of P by XBOOLE_1:8;
now__::_thesis:_not_Ca_is_strong-chain
assume A19: Ca is strong-chain ; ::_thesis: contradiction
a in {a} by TARSKI:def_1;
then A20: a in Ca by XBOOLE_0:def_3;
A21: not a in C by A12, A18, XBOOLE_0:def_5;
C c= Ca by XBOOLE_1:7;
then C c< Ca by A20, A21, XBOOLE_0:def_8;
hence contradiction by A19, A7; ::_thesis: verum
end;
then consider S being non empty finite Subset of P such that
A22: S3[S,Ca] by Def13;
take S ; ::_thesis: S4[a,S]
take S ; ::_thesis: ( S = S & a in S & S3[S,C \/ {a}] )
thus S = S ; ::_thesis: ( a in S & S3[S,C \/ {a}] )
now__::_thesis:_a_in_S
assume A23: not a in S ; ::_thesis: contradiction
A24: S /\ C c= S /\ Ca
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ C or x in S /\ Ca )
assume x in S /\ C ; ::_thesis: x in S /\ Ca
then ( x in S & x in C ) by XBOOLE_0:def_4;
then ( x in S & x in Ca ) by XBOOLE_0:def_3;
hence x in S /\ Ca by XBOOLE_0:def_4; ::_thesis: verum
end;
S /\ Ca c= S /\ C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ Ca or x in S /\ C )
assume A25: x in S /\ Ca ; ::_thesis: x in S /\ C
then A26: x in S by XBOOLE_0:def_4;
x in Ca by A25, XBOOLE_0:def_4;
then ( x in C or x in {a} ) by XBOOLE_0:def_3;
hence x in S /\ C by A26, A23, TARSKI:def_1, XBOOLE_0:def_4; ::_thesis: verum
end;
then A27: S /\ C = S /\ Ca by A24, XBOOLE_0:def_10;
consider p being Clique-partition of (subrelstr S) such that
A28: card p <= stability# P and
A29: not S2[S,p,C] by A6, Def13;
consider c being set such that
A30: c in p and
A31: S /\ C c= c and
A32: for d being set st d in p & d <> c holds
C /\ d = {} by A29;
for d being set st d in p & d <> c holds
Ca /\ d = {}
proof
let d be set ; ::_thesis: ( d in p & d <> c implies Ca /\ d = {} )
assume that
A33: d in p and
A34: d <> c ; ::_thesis: Ca /\ d = {}
now__::_thesis:_not_Ca_/\_d_<>_{}
assume Ca /\ d <> {} ; ::_thesis: contradiction
then consider x being set such that
A35: x in Ca /\ d by XBOOLE_0:def_1;
A36: x in Ca by A35, XBOOLE_0:def_4;
A37: x in d by A35, XBOOLE_0:def_4;
percases ( x in C or x in {a} ) by A36, XBOOLE_0:def_3;
suppose x in C ; ::_thesis: contradiction
then x in C /\ d by A37, XBOOLE_0:def_4;
hence contradiction by A33, A34, A32; ::_thesis: verum
end;
suppose x in {a} ; ::_thesis: contradiction
then x = a by TARSKI:def_1;
then a in the carrier of (subrelstr S) by A37, A33;
hence contradiction by A23, YELLOW_0:def_15; ::_thesis: verum
end;
end;
end;
hence Ca /\ d = {} ; ::_thesis: verum
end;
hence contradiction by A30, A31, A28, A27, A22; ::_thesis: verum
end;
hence a in S ; ::_thesis: S3[S,C \/ {a}]
thus S3[S,C \/ {a}] by A22; ::_thesis: verum
end;
consider f being Function such that
A38: dom f = A and
A39: for x being set st x in A holds
S4[x,f . x] from CLASSES1:sch_1(A17);
A40: rng f is finite by A38, FINSET_1:8;
set SS = union (rng f);
A41: for x being set st x in rng f holds
x is finite
proof
let x be set ; ::_thesis: ( x in rng f implies x is finite )
assume x in rng f ; ::_thesis: x is finite
then consider a being set such that
A42: a in dom f and
A43: x = f . a by FUNCT_1:def_3;
consider S being non empty finite Subset of P such that
A44: f . a = S and
( a in f . a & S3[S,C \/ {a}] ) by A38, A42, A39;
thus x is finite by A44, A43; ::_thesis: verum
end;
A45: union (rng f) c= the carrier of P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng f) or x in the carrier of P )
assume x in union (rng f) ; ::_thesis: x in the carrier of P
then consider y being set such that
A46: x in y and
A47: y in rng f by TARSKI:def_4;
consider a being set such that
A48: a in dom f and
A49: y = f . a by A47, FUNCT_1:def_3;
consider S being non empty finite Subset of P such that
A50: f . a = S and
( a in f . a & S3[S,C \/ {a}] ) by A38, A48, A39;
thus x in the carrier of P by A46, A49, A50; ::_thesis: verum
end;
A51: A9 c= union (rng f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A9 or x in union (rng f) )
assume A52: x in A9 ; ::_thesis: x in union (rng f)
then consider S being non empty finite Subset of P such that
f . x = S and
A53: x in f . x and
S3[S,C \/ {x}] by A39;
f . x in rng f by A52, A38, FUNCT_1:3;
hence x in union (rng f) by A53, TARSKI:def_4; ::_thesis: verum
end;
then reconsider SS = union (rng f) as non empty finite Subset of P by A41, A40, A45, FINSET_1:7;
set SSp = subrelstr SS;
A54: SS = the carrier of (subrelstr SS) by YELLOW_0:def_15;
consider p being Clique-partition of (subrelstr SS) such that
A55: card p <= stability# P and
A56: not S2[SS,p,C] by A6, Def13;
consider c being set such that
A57: c in p and
A58: SS /\ C c= c and
A59: for d being set st d in p & d <> c holds
C /\ d = {} by A56;
reconsider c = c as Element of p by A57;
A9 = A9 /\ SS by A51, XBOOLE_1:28;
then reconsider A = A9 as non empty finite StableSet of (subrelstr SS) by Th31;
A60: stability# (subrelstr SS) >= card A by Def6;
card p >= stability# (subrelstr SS) by Th46;
then card p >= card A by A60, XXREAL_0:2;
then consider a being Element of A such that
A61: c /\ A = {a} by Th48, A55, A16, A15, A5, XXREAL_0:1;
a in c /\ A by A61, TARSKI:def_1;
then A62: a in c by XBOOLE_0:def_4;
consider S being non empty finite Subset of P such that
A63: f . a = S and
A64: a in f . a and
A65: S3[S,C \/ {a}] by A39;
deffunc H1( set ) -> Element of bool the carrier of P = $1 /\ S;
defpred S5[ set ] means $1 meets S;
set Sp = { H1(e) where e is Element of p : S5[e] } ;
A66: S c= SS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in SS )
assume A67: x in S ; ::_thesis: x in SS
S in rng f by A63, A38, FUNCT_1:3;
hence x in SS by A67, TARSKI:def_4; ::_thesis: verum
end;
then reconsider Sp = { H1(e) where e is Element of p : S5[e] } as a_partition of S by A54, PUA2MSS1:11;
for x being set st x in Sp holds
x is Clique of (subrelstr S)
proof
let x be set ; ::_thesis: ( x in Sp implies x is Clique of (subrelstr S) )
assume x in Sp ; ::_thesis: x is Clique of (subrelstr S)
then consider e being Element of p such that
A68: x = e /\ S and
e meets S ;
e is Clique of (subrelstr SS) by Def11;
then e is Clique of P by Th28;
hence x is Clique of (subrelstr S) by A68, Th29; ::_thesis: verum
end;
then reconsider Sp = Sp as Clique-partition of (subrelstr S) by Def11, YELLOW_0:def_15;
A69: Sp = { H1(e) where e is Element of p : S5[e] } ;
A70: card Sp <= card p from DILWORTH:sch_1(A69);
set cc = c /\ S;
c meets S by A62, A63, A64, XBOOLE_0:3;
then A71: c /\ S in Sp ;
S /\ (C \/ {a}) c= c /\ S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ (C \/ {a}) or x in c /\ S )
assume A72: x in S /\ (C \/ {a}) ; ::_thesis: x in c /\ S
then A73: x in S by XBOOLE_0:def_4;
A74: x in C \/ {a} by A72, XBOOLE_0:def_4;
percases ( x in C or x in {a} ) by A74, XBOOLE_0:def_3;
suppose x in C ; ::_thesis: x in c /\ S
then x in SS /\ C by A73, A66, XBOOLE_0:def_4;
hence x in c /\ S by A73, A58, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose x in {a} ; ::_thesis: x in c /\ S
then x = a by TARSKI:def_1;
hence x in c /\ S by A62, A63, A64, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then consider d being set such that
A75: d in Sp and
A76: d <> c /\ S and
A77: (C \/ {a}) /\ d <> {} by A71, A70, A55, A65, XXREAL_0:2;
consider dd being Element of p such that
A78: d = dd /\ S and
dd meets S by A75;
C /\ dd = {} by A78, A76, A59;
then A79: C /\ d = {} /\ S by A78, XBOOLE_1:16
.= {} ;
(C /\ d) \/ ({a} /\ d) <> {} by A77, XBOOLE_1:23;
then consider x being set such that
A80: x in {a} /\ d by A79, XBOOLE_0:def_1;
( x in {a} & x in d ) by A80, XBOOLE_0:def_4;
then a in d by TARSKI:def_1;
then a in dd by A78, XBOOLE_0:def_4;
then c meets dd by A62, XBOOLE_0:3;
hence contradiction by A78, A76, EQREL_1:def_4; ::_thesis: verum
end;
then stability# P9 < k + 1 by A13, XXREAL_0:1;
then A81: stability# P9 <= k by NAT_1:13;
consider A being finite StableSet of P such that
A82: card A = stability# P by Def6;
A83: stability# P9 = k
proof
percases ( A /\ C = {} or A /\ C <> {} ) ;
supposeA84: A /\ C = {} ; ::_thesis: stability# P9 = k
A c= cP9
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in cP9 )
assume A85: x in A ; ::_thesis: x in cP9
then not x in C by A84, XBOOLE_0:def_4;
hence x in cP9 by A85, XBOOLE_0:def_5; ::_thesis: verum
end;
hence stability# P9 = k by A5, A14, A82, Th45; ::_thesis: verum
end;
suppose A /\ C <> {} ; ::_thesis: stability# P9 = k
then consider x being set such that
A86: x in A /\ C by XBOOLE_0:def_1;
A87: x in A by A86, XBOOLE_0:def_4;
A88: x in C by A86, XBOOLE_0:def_4;
set A9 = A \ {x};
{x} c= A by A87, ZFMISC_1:31;
then A89: A = (A \ {x}) \/ {x} by XBOOLE_1:45;
x in {x} by TARSKI:def_1;
then not x in A \ {x} by XBOOLE_0:def_5;
then A90: card A = (card (A \ {x})) + 1 by A89, CARD_2:41;
A91: A \ {x} c= A by XBOOLE_1:36;
A \ {x} c= cP9
proof
let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in A \ {x} or xx in cP9 )
assume A92: xx in A \ {x} ; ::_thesis: xx in cP9
then A93: xx in A by XBOOLE_0:def_5;
not xx in {x} by A92, XBOOLE_0:def_5;
then xx <> x by TARSKI:def_1;
then not xx in C by A87, A88, A93, A6, Th15;
hence xx in cP9 by A92, XBOOLE_0:def_5; ::_thesis: verum
end;
then A94: A \ {x} c= A /\ cP9 by A91, XBOOLE_1:19;
A /\ cP9 c= A \ {x}
proof
let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in A /\ cP9 or xx in A \ {x} )
assume A95: xx in A /\ cP9 ; ::_thesis: xx in A \ {x}
then A96: xx in A by XBOOLE_0:def_4;
xx in cP9 by A95, XBOOLE_0:def_4;
then x <> xx by A88, XBOOLE_0:def_5;
then not xx in {x} by TARSKI:def_1;
hence xx in A \ {x} by A96, XBOOLE_0:def_5; ::_thesis: verum
end;
then A \ {x} = A /\ cP9 by A94, XBOOLE_0:def_10;
then reconsider A9 = A \ {x} as StableSet of P9 by Th31;
stability# P9 >= card A9 by Def6;
hence stability# P9 = k by A90, A82, A5, A81, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
then consider Cp9 being Clique-partition of P9 such that
A97: card Cp9 = stability# P9 by A4;
set Cp = Cp9 \/ {( the carrier of P \ cP9)};
A98: Cp9 is finite by A97;
cP9 <> the carrier of P by A11, XBOOLE_1:37;
then A99: cP9 c< the carrier of P by XBOOLE_0:def_8;
then reconsider Cp = Cp9 \/ {( the carrier of P \ cP9)} as a_partition of the carrier of P by A12, Th4;
now__::_thesis:_for_x_being_set_st_x_in_Cp_holds_
x_is_Clique_of_P
let x be set ; ::_thesis: ( x in Cp implies b1 is Clique of P )
assume A100: x in Cp ; ::_thesis: b1 is Clique of P
percases ( x in Cp9 or x in {( the carrier of P \ cP9)} ) by A100, XBOOLE_0:def_3;
suppose x in Cp9 ; ::_thesis: b1 is Clique of P
then x is Clique of P9 by Def11;
hence x is Clique of P by Th28; ::_thesis: verum
end;
suppose x in {( the carrier of P \ cP9)} ; ::_thesis: b1 is Clique of P
hence x is Clique of P by A6, A11, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then reconsider Cp = Cp as Clique-partition of P by Def11;
take Cp ; ::_thesis: card Cp = stability# P
not the carrier of P \ cP9 in Cp9
proof
assume the carrier of P \ cP9 in Cp9 ; ::_thesis: contradiction
then the carrier of P c= cP9 \/ cP9 by A12, XBOOLE_1:44;
hence contradiction by A99, XBOOLE_1:60; ::_thesis: verum
end;
hence card Cp = stability# P by A5, A83, A97, A98, CARD_2:41; ::_thesis: verum
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A2, A3);
hence ex C being Clique-partition of R st card C = stability# R by A1; ::_thesis: verum
end;
end;
end;
theorem :: DILWORTH:54
for R being transitive antisymmetric with_finite_clique# RelStr ex A being Coloring of R st card A = clique# R
proof
let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: ex A being Coloring of R st card A = clique# R
defpred S1[ Nat] means for P being transitive antisymmetric with_finite_clique# RelStr st clique# P = $1 holds
ex A being Coloring of P st card A = clique# P;
A1: S1[ 0 ]
proof
let P be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: ( clique# P = 0 implies ex A being Coloring of P st card A = clique# P )
assume A2: clique# P = 0 ; ::_thesis: ex A being Coloring of P st card A = clique# P
then P is empty ;
then reconsider C = {} as Coloring of P by EQREL_1:45;
take C ; ::_thesis: card C = clique# P
thus card C = clique# P by A2; ::_thesis: verum
end;
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 A4: S1[n] ; ::_thesis: S1[n + 1]
let P be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: ( clique# P = n + 1 implies ex A being Coloring of P st card A = clique# P )
assume A5: clique# P = n + 1 ; ::_thesis: ex A being Coloring of P st card A = clique# P
then A6: not P is empty ;
reconsider PP = P as non empty transitive antisymmetric with_finite_clique# RelStr by A5;
set M = maximals PP;
set cP = the carrier of P;
set cPM = the carrier of P \ (maximals PP);
reconsider cPM = the carrier of P \ (maximals PP) as Subset of P ;
set PM = subrelstr cPM;
A7: cPM = the carrier of (subrelstr cPM) by YELLOW_0:def_15;
reconsider PM = subrelstr cPM as transitive antisymmetric with_finite_clique# RelStr ;
consider Ca being finite Clique of PM such that
A8: card Ca = clique# PM by Def4;
A9: Ca is Clique of P by Th28;
consider C being finite Clique of P such that
A10: card C = n + 1 by A5, Def4;
A11: C <> {} by A10;
set cC = C /\ cPM;
reconsider cC = C /\ cPM as finite Clique of PM by Th29;
consider m being Element of P such that
A12: m in C and
A13: m is_maximal_wrt C, the InternalRel of P by A6, A11, BAGORDER:6;
A14: m is_maximal_in C by A13, WAYBEL_4:def_24;
A15: C /\ (maximals PP) = {m}
proof
thus C /\ (maximals PP) c= {m} :: according to XBOOLE_0:def_10 ::_thesis: {m} c= C /\ (maximals PP)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in C /\ (maximals PP) or a in {m} )
assume A16: a in C /\ (maximals PP) ; ::_thesis: a in {m}
then A17: a in C by XBOOLE_0:def_4;
A18: a in maximals PP by A16, XBOOLE_0:def_4;
reconsider a9 = a as Element of P by A16;
A19: a9 is_maximal_in [#] P by A18, Def10;
now__::_thesis:_not_a_<>_m
assume A20: a <> m ; ::_thesis: contradiction
not m < a9 by A17, A14, WAYBEL_4:55;
then not m <= a9 by A20, ORDERS_2:def_6;
then a9 <= m by A12, A17, A20, Th6;
then a9 < m by A20, ORDERS_2:def_6;
hence contradiction by A19, A12, WAYBEL_4:55; ::_thesis: verum
end;
hence a in {m} by TARSKI:def_1; ::_thesis: verum
end;
thus {m} c= C /\ (maximals PP) ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {m} or a in C /\ (maximals PP) )
assume a in {m} ; ::_thesis: a in C /\ (maximals PP)
then A21: a = m by TARSKI:def_1;
now__::_thesis:_a_in_maximals_PP
assume A22: not a in maximals PP ; ::_thesis: contradiction
consider y being Element of P such that
A23: y is_maximal_in [#] P and
A24: ( m = y or m < y ) by A6, Th38;
set Cm = C \/ {y};
now__::_thesis:_C_\/_{y}_is_finite_Clique_of_P
percases ( m = y or m <> y ) ;
suppose m = y ; ::_thesis: C \/ {y} is finite Clique of P
hence C \/ {y} is finite Clique of P by A12, ZFMISC_1:40; ::_thesis: verum
end;
suppose m <> y ; ::_thesis: C \/ {y} is finite Clique of P
then m <= y by A24, ORDERS_2:def_6;
hence C \/ {y} is finite Clique of P by A14, Th11; ::_thesis: verum
end;
end;
end;
then reconsider Cm = C \/ {y} as finite Clique of P ;
not y in C by A21, A22, A23, Def10, A24, A14, WAYBEL_4:55;
then card Cm = (card C) + 1 by CARD_2:41;
then (n + 1) + 1 <= (n + 1) + 0 by A10, A5, Def4;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
hence a in C /\ (maximals PP) by A21, A12, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
A25: cC = (C /\ the carrier of P) \ (C /\ (maximals PP)) by XBOOLE_1:50;
C /\ the carrier of P = C by XBOOLE_1:28;
then A26: card cC = (card C) - (card {m}) by A12, A15, A25, EULER_1:4
.= (n + 1) - 1 by A10, CARD_1:30
.= n ;
A27: clique# PM >= card cC by Def4;
A28: clique# PM <= clique# P by Th42;
now__::_thesis:_not_clique#_PM_=_n_+_1
assume A29: clique# PM = n + 1 ; ::_thesis: contradiction
then A30: Ca <> {} by A8;
A31: not PM is empty by A29;
then consider x being Element of PM such that
A32: x in Ca and
A33: x is_maximal_wrt Ca, the InternalRel of PM by A30, BAGORDER:6;
A34: x is_maximal_in Ca by A33, WAYBEL_4:def_24;
reconsider x9 = x as Element of P by A31, YELLOW_0:58;
consider y being Element of P such that
A35: y is_maximal_in [#] P and
A36: ( x9 = y or x9 < y ) by Th38;
set Cb = Ca \/ {y};
now__::_thesis:_Ca_\/_{y}_is_finite_Clique_of_P
percases ( x9 = y or x9 <> y ) ;
suppose x9 = y ; ::_thesis: Ca \/ {y} is finite Clique of P
hence Ca \/ {y} is finite Clique of P by A32, A9, ZFMISC_1:40; ::_thesis: verum
end;
suppose x9 <> y ; ::_thesis: Ca \/ {y} is finite Clique of P
then x9 <= y by A36, ORDERS_2:def_6;
hence Ca \/ {y} is finite Clique of P by A34, Th32, A9, Th11; ::_thesis: verum
end;
end;
end;
then reconsider Cb = Ca \/ {y} as finite Clique of P ;
y in maximals PP by A35, Def10;
then not y in Ca by A7, XBOOLE_0:def_5;
then A37: card Cb = (n + 1) + 1 by A8, A29, CARD_2:41;
card Cb <= n + 1 by A5, Def4;
then n + 1 <= n + 0 by A37, XREAL_1:6;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
then clique# PM < n + 1 by A5, A28, XXREAL_0:1;
then clique# PM <= n by NAT_1:13;
then clique# PM = n by A26, A27, XXREAL_0:1;
then consider Aa being Coloring of PM such that
A38: card Aa = n by A4;
reconsider Ab = Aa as finite set by A38;
set A = Aa \/ {(maximals PP)};
A39: the carrier of P = cPM \/ (maximals PP) by XBOOLE_1:45;
{(maximals PP)} is a_partition of maximals PP by EQREL_1:39;
then A40: Aa \/ {(maximals PP)} is a_partition of the carrier of P by A39, A7, Th3, XBOOLE_1:79;
now__::_thesis:_for_x_being_set_st_x_in_Aa_\/_{(maximals_PP)}_holds_
x_is_StableSet_of_P
let x be set ; ::_thesis: ( x in Aa \/ {(maximals PP)} implies b1 is StableSet of P )
assume A41: x in Aa \/ {(maximals PP)} ; ::_thesis: b1 is StableSet of P
percases ( x in Aa or x in {(maximals PP)} ) by A41, XBOOLE_0:def_3;
suppose x in Aa ; ::_thesis: b1 is StableSet of P
then x is StableSet of PM by Def12;
hence x is StableSet of P by Th30; ::_thesis: verum
end;
suppose x in {(maximals PP)} ; ::_thesis: b1 is StableSet of P
hence x is StableSet of P by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then reconsider A = Aa \/ {(maximals PP)} as Coloring of P by A40, Def12;
take A ; ::_thesis: card A = clique# P
not maximals PP in Ab by A7, XBOOLE_1:38;
hence card A = clique# P by A5, A38, CARD_2:41; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A1, A3);
hence ex A being Coloring of R st card A = clique# R ; ::_thesis: verum
end;
begin
theorem Th55: :: DILWORTH:55
for R being finite transitive antisymmetric RelStr
for r, s being Nat holds
( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )
proof
let R be finite transitive antisymmetric RelStr ; ::_thesis: for r, s being Nat holds
( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )
let r, s be Nat; ::_thesis: ( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )
assume that
A1: card R = (r * s) + 1 and
A2: for C being Clique of R holds card C < r + 1 and
A3: for A being StableSet of R holds card A < s + 1 ; ::_thesis: contradiction
consider p being Clique-partition of R such that
A4: card p = stability# R by Th51;
consider A being finite StableSet of R such that
A5: card A = stability# R by Def6;
stability# R < s + 1 by A3, A5;
then A6: stability# R <= s by NAT_1:13;
set wR = stability# R;
set cR = the carrier of R;
set f = canFS p;
A7: len (canFS p) = card p by UPROOTS:3;
A8: dom (canFS p) = Seg (len (canFS p)) by FINSEQ_1:def_3;
set f = canFS p;
A9: rng (canFS p) = p by FUNCT_2:def_3;
then reconsider f = canFS p as FinSequence of bool the carrier of R by FINSEQ_1:def_4;
now__::_thesis:_for_d,_e_being_Nat_st_d_in_dom_f_&_e_in_dom_f_&_d_<>_e_holds_
f_._d_misses_f_._e
let d, e be Nat; ::_thesis: ( d in dom f & e in dom f & d <> e implies f . d misses f . e )
assume that
A10: d in dom f and
A11: e in dom f and
A12: d <> e ; ::_thesis: f . d misses f . e
A13: f . d in rng f by A10, FUNCT_1:3;
A14: f . e in rng f by A11, FUNCT_1:3;
then reconsider fd = f . d, fe = f . e as Subset of the carrier of R by A13, A9;
fd <> fe by A12, A10, A11, FUNCT_1:def_4;
hence f . d misses f . e by A13, A14, A9, EQREL_1:def_4; ::_thesis: verum
end;
then A15: card (union (rng f)) = Sum (Card f) by A7, INT_5:48;
reconsider n9 = r as Element of NAT by ORDINAL1:def_12;
reconsider h = (stability# R) |-> n9 as Element of (stability# R) -tuples_on NAT ;
A16: Sum h = (stability# R) * r by RVSUM_1:80;
dom f = dom (Card f) by CARD_3:def_2;
then len (Card f) = stability# R by A7, A4, FINSEQ_3:29;
then reconsider Cf = Card f as Element of (stability# R) -tuples_on NAT by FINSEQ_2:92;
A17: h is Element of (stability# R) -tuples_on REAL by FINSEQ_2:109;
A18: Cf is Element of (stability# R) -tuples_on REAL by FINSEQ_2:109;
now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(stability#_R)_holds_
Cf_._j_<=_h_._j
let j be Nat; ::_thesis: ( j in Seg (stability# R) implies Cf . j <= h . j )
assume A19: j in Seg (stability# R) ; ::_thesis: Cf . j <= h . j
A20: h . j = r by A19, FINSEQ_2:57;
A21: Cf . j = card (f . j) by A19, A7, A8, A4, CARD_3:def_2;
f . j in p by A9, A19, A4, A7, A8, FUNCT_1:3;
then reconsider fj = f . j as Clique of R by Def11;
card fj < r + 1 by A2;
hence Cf . j <= h . j by A20, A21, NAT_1:13; ::_thesis: verum
end;
then A22: Sum Cf <= Sum h by A17, A18, RVSUM_1:82;
(stability# R) * r <= s * r by A6, XREAL_1:64;
then Sum Cf <= s * r by A16, A22, XXREAL_0:2;
then (r * s) + 1 <= (r * s) + 0 by A15, A9, A1, EQREL_1:def_4;
hence contradiction by XREAL_1:6; ::_thesis: verum
end;
theorem :: DILWORTH:56
for f being real-valued FinSequence
for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds
ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
proof
let f be real-valued FinSequence; ::_thesis: for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds
ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
let n be Nat; ::_thesis: ( card f = (n ^2) + 1 & f is one-to-one implies ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) )
assume that
A1: card f = (n ^2) + 1 and
A2: f is one-to-one ; ::_thesis: ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
set cP = f;
defpred S1[ set , set ] means ex i, j being Nat ex r, s being real number st
( $1 = [i,r] & $2 = [j,s] & i < j & r < s );
consider iP being Relation of f,f such that
A3: for x, y being set holds
( [x,y] in iP iff ( x in f & y in f & S1[x,y] ) ) from RELSET_1:sch_1();
set P = RelStr(# f,iP #);
A4: dom f = Seg (len f) by FINSEQ_1:def_3;
A5: RelStr(# f,iP #) is antisymmetric
proof
let x, y be set ; :: according to RELAT_2:def_4,ORDERS_2:def_4 ::_thesis: ( not x in the carrier of RelStr(# f,iP #) or not y in the carrier of RelStr(# f,iP #) or not [x,y] in the InternalRel of RelStr(# f,iP #) or not [y,x] in the InternalRel of RelStr(# f,iP #) or x = y )
assume that
x in the carrier of RelStr(# f,iP #) and
y in the carrier of RelStr(# f,iP #) and
A6: [x,y] in the InternalRel of RelStr(# f,iP #) and
A7: [y,x] in the InternalRel of RelStr(# f,iP #) ; ::_thesis: x = y
consider i, j being Nat, r, s being real number such that
A8: x = [i,r] and
A9: y = [j,s] and
A10: ( i < j & r < s ) by A6, A3;
consider j1, i1 being Nat, s1, r1 being real number such that
A11: y = [j1,s1] and
A12: x = [i1,r1] and
A13: ( j1 < i1 & s1 < r1 ) by A7, A3;
( i = i1 & j = j1 ) by A8, A9, A11, A12, XTUPLE_0:1;
hence x = y by A10, A13; ::_thesis: verum
end;
RelStr(# f,iP #) is transitive
proof
let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of RelStr(# f,iP #) or not y in the carrier of RelStr(# f,iP #) or not z in the carrier of RelStr(# f,iP #) or not [x,y] in the InternalRel of RelStr(# f,iP #) or not [y,z] in the InternalRel of RelStr(# f,iP #) or [x,z] in the InternalRel of RelStr(# f,iP #) )
assume that
A14: x in the carrier of RelStr(# f,iP #) and
y in the carrier of RelStr(# f,iP #) and
A15: z in the carrier of RelStr(# f,iP #) and
A16: [x,y] in the InternalRel of RelStr(# f,iP #) and
A17: [y,z] in the InternalRel of RelStr(# f,iP #) ; ::_thesis: [x,z] in the InternalRel of RelStr(# f,iP #)
consider ix, jy being Nat, rx, sy being real number such that
A18: x = [ix,rx] and
A19: y = [jy,sy] and
A20: ( ix < jy & rx < sy ) by A16, A3;
consider iy, jz being Nat, ry, sz being real number such that
A21: y = [iy,ry] and
A22: z = [jz,sz] and
A23: ( iy < jz & ry < sz ) by A17, A3;
( jy = iy & sy = ry ) by A19, A21, XTUPLE_0:1;
then ( ix < jz & rx < sz ) by A20, A23, XXREAL_0:2;
hence [x,z] in the InternalRel of RelStr(# f,iP #) by A18, A22, A14, A15, A3; ::_thesis: verum
end;
then reconsider P = RelStr(# f,iP #) as finite transitive antisymmetric RelStr by A5;
A24: card P = card f ;
percases ( ex C being Clique of P st card C >= n + 1 or ex A being StableSet of P st card A >= n + 1 ) by A24, A1, Th55;
suppose ex C being Clique of P st card C >= n + 1 ; ::_thesis: ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
then consider C being Clique of P such that
A25: card C >= n + 1 ;
set g = C;
reconsider g = C as Subset of f ;
reconsider g = g as Function ;
dom g c= Seg (len f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in Seg (len f) )
assume x in dom g ; ::_thesis: x in Seg (len f)
then consider y being set such that
A26: [x,y] in g by XTUPLE_0:def_12;
x in dom f by A26, XTUPLE_0:def_12;
hence x in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum
end;
then reconsider g = g as FinSubsequence by FINSEQ_1:def_12;
reconsider g = g as real-valued FinSubsequence ;
take g ; ::_thesis: ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus g c= f ; ::_thesis: ( card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus card g >= n + 1 by A25; ::_thesis: ( g is increasing or g is decreasing )
g is increasing
proof
let e1, e2 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: ( not e1 in dom g or not e2 in dom g or e2 <= e1 or not g . e2 <= g . e1 )
assume that
A27: e1 in dom g and
A28: e2 in dom g and
A29: e1 < e2 ; ::_thesis: not g . e2 <= g . e1
A30: [e1,(g . e1)] in g by A27, FUNCT_1:1;
A31: [e2,(g . e2)] in g by A28, FUNCT_1:1;
then reconsider p1 = [e1,(g . e1)], p2 = [e2,(g . e2)] as Element of P by A30;
A32: p1 <> p2 by A29, XTUPLE_0:1;
percases ( p1 <= p2 or p2 <= p1 ) by A30, A31, A32, Th6;
suppose p1 <= p2 ; ::_thesis: not g . e2 <= g . e1
then [p1,p2] in iP by ORDERS_2:def_5;
then consider i, j being Nat, r, s being real number such that
A33: p1 = [i,r] and
A34: p2 = [j,s] and
A35: ( i < j & r < s ) by A3;
( j = e2 & s = g . e2 ) by A34, XTUPLE_0:1;
hence g . e1 < g . e2 by A35, A33, XTUPLE_0:1; ::_thesis: verum
end;
suppose p2 <= p1 ; ::_thesis: not g . e2 <= g . e1
then [p2,p1] in iP by ORDERS_2:def_5;
then consider i, j being Nat, r, s being real number such that
A36: p2 = [i,r] and
A37: p1 = [j,s] and
A38: ( i < j & r < s ) by A3;
( i = e2 & j = e1 ) by A36, A37, XTUPLE_0:1;
hence g . e1 < g . e2 by A29, A38; ::_thesis: verum
end;
end;
end;
hence ( g is increasing or g is decreasing ) ; ::_thesis: verum
end;
suppose ex A being StableSet of P st card A >= n + 1 ; ::_thesis: ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
then consider A being StableSet of P such that
A39: card A >= n + 1 ;
set g = A;
reconsider g = A as Subset of f ;
reconsider g = g as Function ;
A40: dom g c= Seg (len f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in Seg (len f) )
assume x in dom g ; ::_thesis: x in Seg (len f)
then consider y being set such that
A41: [x,y] in g by XTUPLE_0:def_12;
x in dom f by A41, XTUPLE_0:def_12;
hence x in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum
end;
then reconsider g = g as FinSubsequence by FINSEQ_1:def_12;
reconsider g = g as real-valued FinSubsequence ;
take g ; ::_thesis: ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus g c= f ; ::_thesis: ( card g >= n + 1 & ( g is increasing or g is decreasing ) )
thus card g >= n + 1 by A39; ::_thesis: ( g is increasing or g is decreasing )
g is decreasing
proof
let e1, e2 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: ( not e1 in dom g or not e2 in dom g or e2 <= e1 or not g . e1 <= g . e2 )
assume that
A42: e1 in dom g and
A43: e2 in dom g and
A44: e1 < e2 ; ::_thesis: not g . e1 <= g . e2
A45: [e1,(g . e1)] in g by A42, FUNCT_1:1;
A46: [e2,(g . e2)] in g by A43, FUNCT_1:1;
then reconsider p1 = [e1,(g . e1)], p2 = [e2,(g . e2)] as Element of P by A45;
A47: p1 <> p2 by A44, XTUPLE_0:1;
( g . e1 = f . e1 & g . e2 = f . e2 ) by A42, A43, GRFUNC_1:2;
then A48: g . e1 <> g . e2 by A4, A40, A42, A43, A44, A2, FUNCT_1:def_4;
reconsider i = e1, j = e2 as Nat by A42, A43;
reconsider r = g . e1, s = g . e2 as real number ;
A49: ( p1 = [i,r] & p2 = [j,s] ) ;
percases ( g . e1 < g . e2 or g . e1 > g . e2 ) by A48, XXREAL_0:1;
suppose g . e1 < g . e2 ; ::_thesis: not g . e1 <= g . e2
then [p1,p2] in iP by A45, A3, A44, A49;
then p1 <= p2 by ORDERS_2:def_5;
hence g . e1 > g . e2 by A45, A46, A47, Def2; ::_thesis: verum
end;
suppose g . e1 > g . e2 ; ::_thesis: not g . e1 <= g . e2
hence not g . e1 <= g . e2 ; ::_thesis: verum
end;
end;
end;
hence ( g is increasing or g is decreasing ) ; ::_thesis: verum
end;
end;
end;