:: Dilworth's Decomposition Theorem for Posets
:: by Piotr Rudnicki
::
:: Received September 17, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSET_1, XBOOLE_0, CARD_1, XXREAL_0, SUBSET_1, TARSKI,
ORDINAL1, SETFAM_1, ZFMISC_1, EQREL_1, NAT_1, FUNCT_1, FINSEQ_1, ARYTM_3,
RELAT_1, ORDERS_2, RELAT_2, COMBGRAS, STRUCT_0, ORDERS_1, CIRCUIT2,
GROUP_10, RAMSEY_1, JORDAN4, WAYBEL_0, WAYBEL_4, YELLOW_0, FUNCT_2,
LEXBFS, ARYTM_1, UPROOTS, CARD_3, FINSEQ_2, VALUED_0, SQUARE_1, ORDINAL2,
DILWORTH, REAL_1;
notations TARSKI, RELAT_1, RELAT_2, RELSET_1, FINSET_1, SETFAM_1, XBOOLE_0,
SUBSET_1, CARD_1, STRUCT_0, WAYBEL_0, WAYBEL_4, ORDERS_2, ORDINAL1,
EQREL_1, FUNCT_1, FUNCT_2, NUMBERS, XREAL_0, XXREAL_0, NAT_1, YELLOW_0,
XCMPLX_0, ZFMISC_1, LEXBFS, FINSEQ_1, SQUARE_1, UPROOTS, RVSUM_1, INT_5,
FINSEQ_2, VALUED_0, GROUP_10, RAMSEY_1, DOMAIN_1;
constructors DOMAIN_1, LEXBFS, WAYBEL_4, SQUARE_1, UPROOTS, WSIERP_1, INT_5,
RAMSEY_1, RELSET_1, BINOP_2, NUMBERS;
registrations STRUCT_0, XXREAL_0, RELSET_1, CARD_1, YELLOW_0, XREAL_0,
FINSET_1, XBOOLE_0, NAT_1, INT_1, YELLOW_2, EQREL_1, FINSEQ_1, FUNCT_1,
SUBSET_1, ORDINAL1, PEPIN, RVSUM_1, FUNCT_2, FINSEQ_2, RELAT_1, VALUED_0,
ORDERS_2;
requirements ARITHM, SUBSET, BOOLE, NUMERALS, REAL;
definitions TARSKI, FUNCT_1, RELAT_2, XBOOLE_0, VALUED_0, ORDERS_2;
equalities STRUCT_0, WAYBEL_0, SQUARE_1, GROUP_10, ORDINAL1;
expansions TARSKI, FUNCT_1, RELAT_2, XBOOLE_0, ORDERS_2;
theorems CARD_1, CARD_2, NAT_1, XREAL_1, YELLOW_0, XBOOLE_0, TARSKI, ORDERS_2,
XBOOLE_1, ZFMISC_1, EQREL_1, INT_1, EULER_1, ENUMSET1, FUNCT_1, FUNCT_2,
LEXBFS, FINSEQ_4, BAGORDER, WAYBEL_0, WAYBEL_4, XXREAL_0, RELAT_1,
ORDERS_1, FINSET_1, ORDINAL1, PUA2MSS1, DICKSON, FINSEQ_1, INT_5,
RVSUM_1, FINSEQ_2, CARD_3, FINSEQ_3, GRFUNC_1, RAMSEY_1, SUBSET_1,
PRE_POLY, XTUPLE_0, NUMBERS;
schemes NAT_1, FUNCT_2, XBOOLE_0, CLASSES1, FRAENKEL, TREES_2, RELSET_1;
begin :: Preliminaries
:: Facts that I could not find in MML.
scheme FraenkelFinCard1 { A() -> finite non empty set, P[set],
Y() -> finite set, F(set) -> set }:
card Y() <= card A()
provided
A1: Y() = { F(w) where w is Element of A(): P[w] }
proof
A2: A() is finite;
set Z = { F(w) where w is Element of A(): w in A() };
Z is finite from FRAENKEL:sch 21 (A2);
then reconsider Z as finite set;
A3: Z = { F(w) where w is Element of A(): w in A() };
A4: card Z <= card A() from TREES_2:sch 3(A3);
Y() c= Z proof
let x be object;
assume x in Y();
then ex w being Element of A() st x = F(w) & P[w] by A1;
hence x in Z;
end;
then card Y() <= card Z by NAT_1:43;
hence card Y() <= card A() by A4,XXREAL_0:2;
end;
theorem Th1: :: set00:
for X, Y, x being set st not x in X holds X \ (Y \/ {x}) = X \ Y
proof
let X, Y, x be set;
assume not x in X;
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;
end;
theorem Th2: :: ssf0:
for X, Y being set, F being Subset-Family of X, G being Subset-Family of Y
holds F \/ G is Subset-Family of X \/ Y
proof
let X, Y be set, F be Subset-Family of X, G be Subset-Family of 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;
end;
theorem Th3: :: SPpart0:
for X, Y being set, F being a_partition of X, 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, F be a_partition of X, G be a_partition of Y such that
A1: X misses Y;
set PR = F \/ G; set XY = X \/ Y;
A2: PR is Subset-Family of XY by Th2;
A3: union PR = union F \/ union G by ZFMISC_1:78
.= X \/ union G by EQREL_1:def 4 .= X \/ Y by EQREL_1:def 4;
now
let A be Subset of XY such that
A4: A in PR;
A in F or A in G by A4,XBOOLE_0:def 3;
hence A <> {};
let B be Subset of XY such that
A5: B in PR;
per cases by A4,A5,XBOOLE_0:def 3;
suppose A in F & B in F or A in G & B in G;
hence A = B or A misses B by EQREL_1:def 4;
end;
suppose A in F & B in G or A in G & B in F;
hence A = B or A misses B by A1,XBOOLE_1:64;
end;
end;
hence F \/ G is a_partition of X \/ Y by A2,A3,EQREL_1:def 4;
end;
theorem Th4: :: SPpart:
for X, Y being set, 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, F be a_partition of Y;
assume A1: Y c< X;
then A2: X \ Y <> {} by XBOOLE_1:105;
Y c= X by A1;
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;
end;
theorem Th5: :: Sinfset:
for X being infinite set, n being Nat
ex Y being finite Subset of X st card Y > n
proof :: DICKSON:3
let X be infinite set, n be Nat;
consider f being sequence of X such that
A1: f is one-to-one by DICKSON:3;
set Sn = Seg (n+1);
reconsider ff = f|Sn as Function of Sn, 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;
dom ff = Sn by FUNCT_2:def 1;
then card dom ff = n+1 by FINSEQ_1:57;
hence card Y > n by A2,NAT_1:13;
end;
begin :: Cliques and stable sets
definition
let R be RelStr, S be Subset of R;
attr S is connected means :Def1:
the InternalRel of R is_connected_in S;
end;
notation
let R be RelStr, S be Subset of R;
synonym S is clique for S is connected;
end;
registration
let R be RelStr;
cluster trivial -> clique for Subset of R;
coherence proof let S be Subset of R;
assume A1: S is trivial;
let x1, x2 be object;
thus thesis by A1,ZFMISC_1:def 10;
end;
end;
registration
let R be RelStr;
cluster clique for Subset of R;
existence proof take {}R; let x1, x2 be object; thus thesis; end;
end;
definition
let R be RelStr;
mode Clique of R is clique Subset of R;
end;
theorem Th6: :: DClique:
for R being RelStr, 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 holds a <= b or b <= a
proof
let R be RelStr, S be Subset of R;
set RR = the InternalRel of R;
hereby
assume S is Clique of R;
then A1: RR is_connected_in S by Def1;
let a, b be Element of R;
assume a in S & b in S & a <> b;
then [a,b] in RR or [b,a] in RR by A1;
hence a <= b or b <= a;
end;
assume
A2: for a, b being Element of R st a in S & b in S & a <> b
holds a <= b or b <= a;
RR is_connected_in S proof
let x, y be object;
assume A3: x in S & y in S & x <> y;
then reconsider x9 = x, y9 = y as Element of R;
x9 <= y9 or y9 <= x9 by A3,A2;
hence [x,y] in RR or [y,x] in RR;
end;
hence S is Clique of R by Def1;
end;
registration
let R be RelStr;
cluster finite for Clique of R;
existence proof take {}R; thus thesis; end;
end;
registration
let R be reflexive RelStr;
cluster connected -> strongly_connected for Subset of R;
coherence proof
let C be Subset of R;
set iR = the InternalRel of R, cR = the carrier of R;
assume C is clique;
then A1: iR is_connected_in C;
A2: iR is_reflexive_in cR by ORDERS_2:def 2;
thus C is strongly_connected proof
let x, y be object such that
A3: x in C and
A4: y in C;
per cases;
suppose x = y;
hence [x,y] in the InternalRel of R or [y,x] in the InternalRel of R
by A3,A2;
end;
suppose x <> y;
hence [x,y] in the InternalRel of R or [y,x] in the InternalRel of R
by A3,A4,A1;
end;
end;
end;
end;
registration
let R be non empty RelStr;
cluster finite non empty for Clique of R;
existence proof
{the Element of R} is clique;
hence thesis;
end;
end;
theorem :: Clique36a:
for R being non empty RelStr, a1,a2 being Element of R
st a1 <> a2 & {a1,a2} is Clique of R holds a1 <= a2 or a2 <= a1
proof
let R be non empty RelStr, a1,a2 be Element of R;
assume A1: a1 <> a2;
A2: a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
assume {a1,a2} is Clique of R;
hence thesis by A2,A1,Th6;
end;
theorem Th8: :: Clique36b:
for R being non empty RelStr, 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, a1,a2 be Element of R;
assume A1: a1 <= a2 or a2 <= a1;
now
let x,y be Element of R;
assume x in {a1,a2} & y in {a1,a2};
then A2: (x = a1 or x = a2) & (y = a1 or y = a2) by TARSKI:def 2;
assume x <> y;
hence x <= y or y <= x by A1,A2;
end;
hence thesis by Th6;
end;
theorem Th9: :: Clique37:
for R being RelStr, C being Clique of R, S being Subset of C
holds S is Clique of R
proof
let R be RelStr, C be Clique of R, S be Subset of C;
set iR = the InternalRel of R;
A1: iR is_connected_in C by Def1;
iR is_connected_in S by A1;
hence thesis by Def1,XBOOLE_1:1;
end;
theorem :: Clique1:
for R being RelStr, C being finite Clique of R, n being Nat
st n <= card C ex B being finite Clique of R st B c= C & card B = n
proof
let R be RelStr, C be finite Clique of R, n be Nat such that
A1: n <= card C;
consider BB being finite Subset of C such that
A2: card BB = n by A1,FINSEQ_4:72;
reconsider BB as finite Clique of R by Th9;
take BB;
thus thesis by A2;
end;
theorem Th11: :: ExtClique
for R being transitive RelStr, C being Clique of R, 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, C be Clique of R, x, y be Element of R such that
A1: x is_maximal_in C and
A2: x <= y;
A3: x in C by A1,WAYBEL_4:55;
A4: the carrier of R is non empty by A1,WAYBEL_4:55;
set Cb = C \/ {y};
A5: Cb c= the carrier of R proof
let x be object;
assume A6: x in Cb;
per cases by A6,XBOOLE_0:def 3;
suppose x in C;
hence x in the carrier of R;
end;
suppose x in {y};
then x = y by TARSKI:def 1;
hence x in the carrier of R by A4;
end;
end;
now
let a, b be Element of R such that
A7: a in Cb & b in Cb and
A8: a <> b;
per cases by A7,XBOOLE_0:def 3;
suppose a in C & b in C;
hence a <= b or b <= a by A8,Th6;
end;
suppose that
A9: a in C and
A10: b in {y};
A11: b = y by A10,TARSKI:def 1;
A12: not x < a by A1,A9,WAYBEL_4:55;
per cases;
suppose x <> a;
then a <= x or x <= a by A9,A3,Th6;
hence a <= b or b <= a by A2,A11,A12,ORDERS_2:3;
end;
suppose x = a;
hence a <= b or b <= a by A2,A10,TARSKI:def 1;
end;
end;
suppose that
A13: a in {y} and
A14: b in C;
A15: a = y by A13,TARSKI:def 1;
A16: not x < b by A1,A14,WAYBEL_4:55;
per cases;
suppose x <> b;
then b <= x or x <= b by A14,A3,Th6;
hence a <= b or b <= a by A2,A15,A16,ORDERS_2:3;
end;
suppose x = b;
hence a <= b or b <= a by A2,A13,TARSKI:def 1;
end;
end;
suppose a in {y} & b in {y};
then a = y & b = y by TARSKI:def 1;
hence a <= b or b <= a by A8;
end;
end;
hence C \/ {y} is Clique of R by A5,Th6;
end;
theorem Th12: :: ExtCliquemin
for R being transitive RelStr, C being Clique of R, 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, C be Clique of R, x, y be Element of R such that
A1: x is_minimal_in C and
A2: y <= x;
A3: x in C by A1,WAYBEL_4:56;
A4: the carrier of R is non empty by A1,WAYBEL_4:56;
set Cb = C \/ {y};
A5: Cb c= the carrier of R proof
let x be object;
assume A6: x in Cb;
per cases by A6,XBOOLE_0:def 3;
suppose x in C;
hence x in the carrier of R;
end;
suppose x in {y};
then x = y by TARSKI:def 1;
hence x in the carrier of R by A4;
end;
end;
now
let a, b be Element of R such that
A7: a in Cb & b in Cb and
A8: a <> b;
per cases by A7,XBOOLE_0:def 3;
suppose a in C & b in C;
hence a <= b or b <= a by A8,Th6;
end;
suppose that
A9: a in C and
A10: b in {y};
A11: b = y by A10,TARSKI:def 1;
A12: not a < x by A1,A9,WAYBEL_4:56;
per cases;
suppose A13: a <> x;
then not a <= x by A12;
then x <= a by A9,A3,A13,Th6;
hence a <= b or b <= a by A2,A11,ORDERS_2:3;
end;
suppose x = a;
hence a <= b or b <= a by A2,A10,TARSKI:def 1;
end;
end;
suppose that
A14: a in {y} and
A15: b in C;
A16: a = y by A14,TARSKI:def 1;
A17: not b < x by A1,A15,WAYBEL_4:56;
per cases;
suppose A18: b <> x;
then not b <= x by A17;
then x <= b by A15,A3,A18,Th6;
hence a <= b or b <= a by A2,A16,ORDERS_2:3;
end;
suppose x = b;
hence a <= b or b <= a by A2,A14,TARSKI:def 1;
end;
end;
suppose a in {y} & b in {y};
then a = y & b = y by TARSKI:def 1;
hence a <= b or b <= a by A8;
end;
end;
hence C \/ {y} is Clique of R by A5,Th6;
end;
definition
let R be RelStr, S be Subset of R;
attr S is stable means :Def2:
for x, y being Element of R st x in S & y in S & x <> y
holds not x <= y & not y <= x;
end;
registration
let R be RelStr;
cluster trivial -> stable for Subset of R;
coherence
by ZFMISC_1:def 10;
end;
registration
let R be RelStr;
cluster stable for Subset of R;
existence proof
reconsider A = {} as Subset of R by XBOOLE_1:2;
take A;
let x, y be Element of R;
thus thesis;
end;
end;
definition
let R be RelStr;
mode StableSet of R is stable Subset of R;
:: other possible names: AntiChain of R, IndependentSet of R
end;
registration
let R be RelStr;
cluster finite for StableSet of R;
existence proof
take {}R;
thus thesis;
end;
end;
registration
let R be non empty RelStr;
cluster finite non empty for StableSet of R;
existence proof
{the Element of R} is stable;
hence thesis;
end;
end;
theorem :: AChain36a:
for R being non empty RelStr, a1, a2 being Element of R
st a1 <> a2 & {a1,a2} is StableSet of R holds not (a1 <= a2 or a2 <= a1)
proof
let R be non empty RelStr, a1,a2 be Element of R;
assume A1: a1 <> a2;
A2: a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
assume {a1,a2} is StableSet of R;
hence thesis by A2,A1,Def2;
end;
theorem Th14: :: AChain36b:
for R being non empty RelStr, a1, a2 being Element of R
st not (a1 <= a2 or a2 <= a1) holds {a1,a2} is StableSet of R
proof
let R be non empty RelStr, a1,a2 be Element of R;
assume
A1: not (a1 <= a2 or a2 <= a1);
set S = {a1,a2};
S is stable proof
let x, y be Element of R such that
A2: x in S & y in S & x <> y;
(x = a1 or x = a2) & (y = a1 or y = a2) by A2,TARSKI:def 2;
hence thesis by A1,A2;
end;
hence thesis;
end;
theorem Th15: :: ACClique:
for R being RelStr, C being Clique of R, A being StableSet of R, 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, C be Clique of R, A be StableSet of R, a, b be set such that
A1: a in A & b in A and
A2: a in C & b in C;
assume A3: a <> b;
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;
end;
theorem Th16: :: AChain0:
for R being RelStr, A being StableSet of R, B being Subset of A
holds B is StableSet of R
proof
let R be RelStr, A be StableSet of R, B be Subset of A;
reconsider BB = B as Subset of R by XBOOLE_1:1;
BB is stable by Def2;
hence thesis;
end;
theorem Th17: :: AChain1:
for R being RelStr, A being finite StableSet of R, n being Nat
st n <= card A ex B being finite StableSet of R st card B = n
proof
let R be RelStr, A be finite StableSet of R, n be Nat such that
A1: n <= card A;
consider BB being finite Subset of A such that
A2: card BB = n by A1,FINSEQ_4:72;
reconsider BB as finite StableSet of R by Th16;
take BB;
thus card BB = n by A2;
end;
begin :: Clique number and stability number
definition
let R be RelStr;
attr R is with_finite_clique# means :Def3:
ex C being finite Clique of R
st for D being finite Clique of R holds card D <= card C;
end;
registration
cluster finite -> with_finite_clique# for RelStr;
coherence proof
let R be RelStr;
assume R is finite;
then reconsider R9 = R as finite RelStr;
defpred P[Nat] means ex c being finite Clique of R st card c = $1;
A1: for k being Nat st P[k] holds k <= card R9 by NAT_1:43;
card {}R = 0; then
A2: ex k being Nat st P[k];
consider k being Nat such that
A3: P[k] and
A4: for n being Nat st P[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 be finite Clique of R holds card(D) <= card(c) by A5,A4;
hence R is with_finite_clique#;
end;
end;
registration
let R be with_finite_clique# RelStr;
cluster -> finite for Clique of R;
coherence proof
let D be Clique of R;
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;
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;
end;
end;
definition
let R be with_finite_clique# RelStr;
func clique# R -> Nat means :Def4:
(ex C being finite Clique of R st card C = it)
& for T being finite Clique of R holds card T <= it;
existence 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;
thus ex A being finite Clique of R st card A = itt;
let T being finite Clique of R;
thus card T <= itt by A1;
end;
uniqueness proof
let it1, it2 be Nat such 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;
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;
end;
end;
registration
let R be empty RelStr;
cluster clique# R -> empty;
coherence proof
for T being Clique of R holds card T <= card {}R;
hence thesis by Def4;
end;
end;
registration
let R be with_finite_clique# non empty RelStr;
cluster clique# R -> positive;
coherence proof
card {the Element of R} <= clique# R by Def4;
hence thesis;
end;
end;
theorem :: Height3:
for R being with_finite_clique# non empty RelStr
st [#]R is StableSet of R holds clique# R = 1
proof
let R be with_finite_clique# non empty RelStr;
assume A1: [#]R is StableSet of R;
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;
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 thesis by A4,A5,A6,A1,Th15;
end;
theorem Th19: :: Height4:
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;
assume A1: clique# R = 1;
set cR = the carrier of R;
A2: R is non empty by A1;
now
let a, b be Element of R such that
a in cR and b in cR and
A3: a <> b;
assume a <= b or b <= a;
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;
end;
hence [#]R is StableSet of R by Def2;
end;
definition
let R be RelStr;
attr R is with_finite_stability# means :Def5:
ex A being finite StableSet of R
st for B being finite StableSet of R holds card B <= card A;
end;
registration
cluster finite -> with_finite_stability# for RelStr;
coherence proof
let R be RelStr;
assume R is finite;
then reconsider R9 = R as finite RelStr;
defpred P[Nat] means
ex A being finite StableSet of R9 st card A = $1;
A1: for k being Nat st P[k] holds k <= card R9 by NAT_1:43;
{}R is StableSet of R & card {} = 0;
then A2: ex k being Nat st P[k];
consider k being Nat such that
A3: P[k] and
A4: for n being Nat st P[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;
let T be finite StableSet of R;
thus card T <= card S by A5,A4;
end;
end;
registration
let R be with_finite_stability# RelStr;
cluster -> finite for StableSet of R;
coherence 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;
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;
end;
end;
definition
let R be with_finite_stability# RelStr;
func stability# R -> Nat means :Def6:
(ex A being finite StableSet of R st card(A) = it)
& for T being finite StableSet of R holds card T <= it;
existence 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;
thus ex A being finite StableSet of R st card A = itt;
let T being finite StableSet of R;
thus card(T) <= itt by A1;
end;
uniqueness proof
let it1, it2 be Nat such 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;
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;
end;
end;
registration
let R be empty RelStr;
cluster stability# R -> empty;
coherence proof
for T being StableSet of R holds card(T) <= card {}R;
hence thesis by Def6;
end;
end;
registration
let R be with_finite_stability# non empty RelStr;
cluster stability# R -> positive;
coherence proof
card{the Element of R} <= stability# R by Def6;
hence thesis;
end;
end;
theorem Th20: :: Width3:
for R being with_finite_stability# non empty RelStr
st [#]R is Clique of R holds stability# R = 1
proof
let R be with_finite_stability# non empty RelStr;
assume A1: [#]R is Clique of R;
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;
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 thesis by A4,A5,A6,A1,Th15;
end;
theorem Th21: :: Width4:
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;
assume A1: stability# R = 1;
set cR = the carrier of R;
now
let a, b be Element of R such that
A2: a in cR and b in cR and
A3: a <> b;
A4: R is non empty by A2;
assume not (a <= b or b <= a);
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;
end;
hence [#]R is Clique of R by Th6;
end;
registration
:: I have done it through Ramsey. How else to prove it?
:: For posets one gets it directly from Dilworth.
:: Related: how big the gap between (clique# * stability#) and
:: card of the carrier can be?
cluster with_finite_clique# with_finite_stability# -> finite for RelStr;
coherence proof
let R be RelStr;
assume A1: R is with_finite_clique#;
assume A2: R is with_finite_stability#;
assume A3: R is infinite;
reconsider 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, w = stability# R;
A6: 0+1 <= h by A3,NAT_1:13;
A7: 0+1 <= w by A3,NAT_1:13;
set cR = the carrier of R;
A8: cR = [#]R;
per cases by A6,A7,XXREAL_0:1;
suppose h = 1;
then A9: cR is StableSet of R by A8,Th19;
consider Y being finite Subset of cR such that
A10: card Y > w by A3,Th5;
Y is StableSet of R by A9,Th16;
hence thesis by A10,Def6;
end;
suppose w = 1;
then A11: cR is Clique of R by A8,Th21;
consider Y being finite Subset of cR such that
A12: card Y > h by A3,Th5;
Y is Clique of R by A11,Th9;
hence thesis by A12,Def4;
end;
suppose A13: h > 1 & w > 1;
set m = max(clique# R, stability# R) +1;
reconsider m as Nat;
consider r being Nat such that
A14: for X being finite set, 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 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 or y <= x) };
set E = the_subsets_of_card(2,X); set P = { A, B };
A17: A c= E proof
let x be object;
reconsider x1=x as set by TARSKI:1;
assume x in A;
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 x1 = 2
by A18,A19,A20,A21,CARD_2:57,ZFMISC_1:32;
hence thesis;
end;
A22: B c= E proof
let x be object;
reconsider x1=x as set by TARSKI:1;
assume x in B;
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 or yy <= xx);
x is Subset of X & card x1 = 2
by A23,A24,A25,A26,CARD_2:57,ZFMISC_1:32;
hence thesis;
end;
A27: A in P & B in P by TARSKI:def 2;
A28: now
assume A29: A = B;
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, b as Element of R by A30,A31;
A33: not (a <= b or 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 B 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;
end;
A36: P c= bool E proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in P;
then xx c= E by A17,A22,TARSKI:def 2;
hence thesis;
end;
A37: union P = E proof
thus union P c= E proof
let x be object;
assume x in union P;
then consider Y being set such that
A38: x in Y and
A39: Y in P by TARSKI:def 4;
Y = A or Y = B by A39,TARSKI:def 2;
hence thesis by A38,A17,A22;
end;
thus E c= union P proof
let x be object;
assume x in E;
then consider xx being Subset of X such that
A40: x = xx and
A41: card xx = 2;
consider a, b being object 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, b as Element of R;
A44: a in xx & b in xx by A43,TARSKI:def 2;
not (a <= b or b <= a) or (a <= b or b <= a);
then {a,b} in A or {a,b} in B by A44,A42;
hence x in union P by A40,A43,A27,TARSKI:def 4;
end;
end;
for a being Subset of E st a in P holds a<>{} &
for b being Subset of E st b in P holds a = b or a misses b proof
let a be Subset of E such that
A45: a in P;
thus a<>{} proof
per cases by A45,TARSKI:def 2;
suppose A46: a = 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, 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 A by A50,A49;
hence thesis by A46;
end;
suppose A51: a = B;
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, bb as Element of R by A52,A53;
A55: not (aa <= bb or 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 B by A55,A54;
hence thesis by A51;
end;
end;
let b be Subset of E such that
A56: b in P;
assume A57: a <> b;
assume A58: a meets b;
(a = A or a = B) & (b = A or b = B) by A45,A56,TARSKI:def 2;
then A /\ B <> {} by A57,A58;
then consider x being object such that
A59: x in A /\ B by XBOOLE_0:def 1;
x in A 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 B 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 or y2 <= x2);
xx = x2 & yy = y2 or xx = y2 & yy = x2 by A60,A62,ZFMISC_1:6;
hence contradiction by A61,A63;
end;
then reconsider P as a_partition of E 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 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;
per cases by TARSKI:def 2;
suppose A69: p = A;
now
let x, y be Element of R such that
A70: x in S and
A71: y in S and
A72: x <> y;
{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 A 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;
end;
then S is Clique of R by Th6;
hence contradiction by A66,Def4;
end;
suppose A75: p = B;
S is stable proof
let x, y being Element of R such that
A76: x in S and
A77: y in S and
A78: x <> y;
{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 B 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 or 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;
end;
hence contradiction by A67,Def6;
end;
end;
end;
end;
begin :: Lower and upper sets, minimal and maximal elements
definition
let R be RelStr, X be Subset of R;
func Lower X -> Subset of R equals
X \/ downarrow X;
coherence;
func Upper X -> Subset of R equals
X \/ uparrow X;
coherence;
end;
theorem Th22: :: ABAC0:
for R being antisymmetric transitive RelStr, A being StableSet of R,
z being set
st z in Upper A & z in Lower A holds z in A
proof
let R be antisymmetric transitive RelStr, A be StableSet of R,
z be set such that
A1: z in Upper A and
A2: z in Lower A;
per cases;
suppose z in A;
hence thesis;
end;
suppose A3: not 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;
end;
end;
theorem Th23: :: ABunion:
for R being with_finite_stability# RelStr, A being StableSet of R
st card A = stability# R holds Upper A \/ Lower A = [#]R
proof
let R be with_finite_stability# RelStr, A be StableSet of R such that
A1: card A = stability# R;
set cP = the carrier of R;
cP c= Upper A \/ Lower A proof
let x be object;
assume A2: x in cP;
assume A3: not x in Upper A \/ Lower A;
reconsider x as Element of cP 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
let a, b be Element of R such that
A9: a in Ax and
A10: b in Ax and
A11: a <> b;
per cases by A9,A10,XBOOLE_0:def 3;
suppose a in A & b in A;
hence not a <= b & not b <= a by A11,Def2;
end;
suppose A12: a in A & b in {x};
then b = x by TARSKI:def 1;
hence not a <= b & not b <= a by A6,A7,A12,WAYBEL_0:def 15,def 16;
end;
suppose A13: a in {x} & b in A;
then a = x by TARSKI:def 1;
hence not a <= b & not b <= a by A6,A7,A13,WAYBEL_0:def 15,def 16;
end;
suppose a in {x} & b in {x};
then a = x & b = x by TARSKI:def 1;
hence not a <= b & not b <= a by A11;
end;
end;
then A14: Ax is StableSet of R by A8,Def2,XBOOLE_1:8;
card Ax = card A + 1 by A5,CARD_2:41;
then card Ax > card A by NAT_1:13;
hence contradiction by Def6,A1,A14;
end;
hence Upper A \/ Lower A = [#]R;
end;
theorem Th24: :: Pminmin:
for R being transitive RelStr, x being Element of R, S being Subset of R
st x is_minimal_in Lower S holds x is_minimal_in [#]R
proof
let R be transitive RelStr, x be Element of R, S be Subset of R such that
A1: x is_minimal_in Lower S;
set cR = the carrier of R;
A2: x in Lower S by A1,WAYBEL_4:56;
assume not x is_minimal_in [#]R;
then consider y being Element of R such that y in cR and
A3: y < x by A2,WAYBEL_4:56;
per cases by A2,XBOOLE_0:def 3;
suppose A4: x in S;
y <= x by A3;
then y in downarrow S by A4,WAYBEL_0:def 15;
then y in Lower S by XBOOLE_0:def 3;
hence thesis by A1,A3,WAYBEL_4:56;
end;
suppose x in downarrow S;
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; 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;
end;
end;
theorem Th25: :: Pmaxmax:
for R being transitive RelStr, x being Element of R, S being Subset of R
st x is_maximal_in Upper S holds x is_maximal_in [#]R
proof
let R be transitive RelStr, x be Element of R, S be Subset of R such that
A1: x is_maximal_in Upper S;
set cR = the carrier of R;
A2: x in Upper S by A1,WAYBEL_4:55;
assume not x is_maximal_in [#]R;
then consider y being Element of R such that y in cR and
A3: x < y by A2,WAYBEL_4:55;
per cases by A2,XBOOLE_0:def 3;
suppose A4: x in S;
x <= y by A3;
then y in uparrow S by A4,WAYBEL_0:def 16;
then y in Upper S by XBOOLE_0:def 3;
hence thesis by A1,A3,WAYBEL_4:55;
end;
suppose x in uparrow S;
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;
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;
end;
end;
definition
let R be RelStr;
set cR = the carrier of R;
func minimals R -> Subset of R means :Def9:
for x being Element of R holds x in it iff x is_minimal_in [#]R
if R is non empty
otherwise it = {};
consistency;
existence proof
defpred P[object] means
ex a being Element of R st a = $1 & a is_minimal_in cR;
consider X being set such that
A1: for x being object holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1;
A2: now
assume A3: cR is non empty;
for x being object st x in X holds x in cR by A1;
then reconsider X as Subset of R by TARSKI:def 3;
take X;
let x be Element of R;
x in X implies P[x] by A1;
hence x in X iff x is_minimal_in cR by A1,A3;
end;
now
reconsider X = {} as Subset of R by XBOOLE_1:2;
take X;
thus X = {};
end;
hence thesis by A2;
end;
uniqueness proof
let it1, it2 be Subset of R;
now assume that R is non empty and
A4: for x being Element of R holds x in it1 iff x is_minimal_in cR and
A5: for x being Element of R holds x in it2 iff x is_minimal_in cR;
for x be object holds x in it1 iff x in it2 by A4,A5;
hence it1 = it2 by TARSKI:2;
end;
hence thesis;
end;
func maximals R -> Subset of R means :Def10:
for x being Element of R holds x in it iff x is_maximal_in [#]R
if R is non empty
otherwise it = {};
consistency;
existence proof
defpred P[object] means
ex a being Element of R st a = $1 & a is_maximal_in cR;
consider X being set such that
A6: for x being object holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1;
A7: now
assume A8: cR is non empty;
for x being object st x in X holds x in cR by A6;
then reconsider X as Subset of R by TARSKI:def 3;
take X;
let x be Element of R;
x in X implies P[x] by A6;
hence x in X iff x is_maximal_in cR by A6,A8;
end;
now
reconsider X = {} as Subset of R by XBOOLE_1:2;
take X;
thus X = {};
end;
hence thesis by A7;
end;
uniqueness proof
let it1, it2 be Subset of R;
now assume that R is non empty and
A9: for x being Element of R holds x in it1 iff x is_maximal_in cR and
A10: for x being Element of R holds x in it2 iff x is_maximal_in cR;
for x being object holds x in it1 iff x in it2 by A9,A10;
hence it1 = it2 by TARSKI:2;
end;
hence thesis;
end;
end;
registration
let R be with_finite_clique# non empty antisymmetric transitive RelStr;
cluster maximals R -> non empty;
coherence proof
set cP = the carrier of R, 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, iP by BAGORDER:6;
A3: y is_maximal_in CL by A2,WAYBEL_4:def 24;
A4: cP = [#]R;
now
assume not y is_maximal_in cP;
then consider z being Element of R such that z in cP and
A5: y < z by WAYBEL_4:55;
A6: y <= z by A5;
set C = CL \/ {z};
reconsider C 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;
end;
hence thesis by A4,Def10;
end;
cluster minimals R -> non empty;
coherence proof
set cP = the carrier of R, 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, iP by BAGORDER:7;
A9: y is_minimal_in CL by A8,WAYBEL_4:def 26;
A10: cP = [#]R;
now
assume not y is_minimal_in cP;
then consider z being Element of R such that z in cP and
A11: z < y by WAYBEL_4:56;
A12: z <= y by A11;
set C = CL \/ {z};
reconsider C 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;
end;
hence thesis by A10,Def9;
end;
end;
registration let R be RelStr;
cluster minimals R -> stable;
coherence
proof
set mR = minimals R;
let x, y be Element of R such that
A1: x in mR and
A2: y in mR and
A3: x <> y;
A4: R is non 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;
x is_minimal_in [#]R by A1,A4,Def9;
then not x > y by A2,WAYBEL_4:56;
hence not y <= x by A3;
end;
cluster maximals R -> stable;
coherence
proof
set mR = maximals R;
let x, y be Element of R such that
A5: x in mR and
A6: y in mR and
A7: x <> y;
A8: R is non 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;
y is_maximal_in [#]R by A6,A8,Def10;
then not x > y by A5,WAYBEL_4:55;
hence not y <= x by A7;
end;
end;
theorem Th26: :: PCAamin:
for R being RelStr, A being StableSet of R
st not minimals R c= A holds not minimals R c= Upper A
proof
let R be RelStr, A be StableSet of R;
assume not minimals R c= A;
then consider x being object such that
A1: x in minimals R and
A2: not x in A;
assume A3: minimals R c= Upper A;
reconsider x9 = x as Element of R by A1;
R is non 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 assume x99 <> x9;
then x99 < x9 by A5;
hence contradiction by A1,A4,WAYBEL_4:56;
end;
hence contradiction by A6,A2;
end;
theorem Th27: :: PCAbmax:
for R being RelStr, A being StableSet of R
st not maximals R c= A holds not maximals R c= Lower A
proof
let R be RelStr, A be StableSet of R such that
A1: not maximals R c= A;
consider x being object such that
A2: x in maximals R and
A3: not x in A by A1;
assume A4: maximals R c= Lower A;
reconsider x9 = x as Element of R by A2;
R is non 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 assume x99 <> x9;
then x9 < x99 by A6;
hence contradiction by A2,A5,WAYBEL_4:55;
end;
hence contradiction by A7,A3;
end;
begin :: Substructures
registration
let R be RelStr, X be finite Subset of R;
cluster subrelstr X -> finite;
coherence by YELLOW_0:def 15;
end;
theorem Th28: :: SPClique:
for R being RelStr, S being Subset of R, C being Clique of subrelstr S
holds C is Clique of R
proof
let R be RelStr, S be Subset of R, C be Clique of subrelstr S;
A1: the carrier of subrelstr S = S by YELLOW_0:def 15;
now
let a, b be Element of R such that
A2: a in C and
A3: b in C and
A4: a <> b;
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;
end;
hence C is Clique of R by A1,Th6,XBOOLE_1:1;
end;
theorem Th29: :: SPClique1:
for R being RelStr, S being Subset of R, C being Clique of R
holds C /\ S is Clique of subrelstr S
proof
let R be RelStr, S be Subset of R, C be Clique of R;
set sS = subrelstr S, CS = C /\ S;
A1: CS c= S by XBOOLE_1:17;
A2: S = the carrier of sS by YELLOW_0:def 15;
now
let a, b be Element of sS;
assume A3: a in CS;
assume A4: b in CS;
assume A5: a <> b;
A6: a in S & b in S by A3,A4,XBOOLE_0:def 4;
A7: S is non empty by A3;
R is non 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;
end;
hence C /\ S is Clique of subrelstr S by Th6,A1,YELLOW_0:def 15;
end;
theorem Th30: :: SPAChain1:
for R being RelStr, S being Subset of R, A being StableSet of subrelstr S
holds A is StableSet of R
proof
let R be RelStr, S be Subset of R, A be StableSet of subrelstr S;
set sS = subrelstr S;
per cases;
suppose R is empty;
then the carrier of sS = {} by YELLOW_0:def 15;
then A = {}R;
hence A is StableSet of R;
end;
suppose A1: R is non empty;
per cases;
suppose S is empty;
then the carrier of sS = {} by YELLOW_0:def 15;
then A = {}R;
hence A is StableSet of R;
end;
suppose A2: S is non empty;
S = the carrier of sS by YELLOW_0:def 15;
then reconsider A as Subset of R by XBOOLE_1:1;
A is stable proof
let x, y be Element of R such that
A3: x in A and
A4: y in A and
A5: x <> y;
reconsider x9 = x, y9 = y as Element of sS 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;
end;
hence thesis;
end;
end;
end;
theorem Th31: :: SPAChain:
for R being RelStr, S being Subset of R, A being StableSet of R
holds A /\ S is StableSet of subrelstr S
proof
let R be RelStr, S be Subset of R, A be StableSet of R;
set sS = subrelstr S, AS = A /\ S;
per cases;
suppose R is empty;
then A /\ S = {}sS;
hence A /\ S is StableSet of sS;
end;
suppose A1: R is non empty;
per cases;
suppose S is empty;
then A /\ S = {}sS;
hence A /\ S is StableSet of sS;
end;
suppose A2: S is non empty;
S = the carrier of sS by YELLOW_0:def 15;
then reconsider AS as Subset of sS by XBOOLE_1:17;
AS is stable proof
let x, y be Element of sS such that
A3: x in AS and
A4: y in AS and
A5: x <> y;
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;
end;
hence A /\ S is StableSet of sS;
end;
end;
end;
theorem Th32: :: SPmax
for R being RelStr, S being Subset of R, B being Subset of subrelstr S,
x being Element of subrelstr S, y being Element of R
st x = y & x is_maximal_in B holds y is_maximal_in B
proof
let R be RelStr, S be Subset of R, B be Subset of subrelstr S,
x be Element of subrelstr S, y be Element of R such that
A1: x = y and
A2: x is_maximal_in B;
A3: x in B by A2,WAYBEL_4:55;
assume not y is_maximal_in B;
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;
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;
hence contradiction by A4,A2,WAYBEL_4:55;
end;
theorem Th33: :: SPmin
for R being RelStr, S being Subset of R, B being Subset of subrelstr S,
x being Element of subrelstr S, y being Element of R
st x = y & x is_minimal_in B holds y is_minimal_in B
proof
let R be RelStr, S be Subset of R, B be Subset of subrelstr S,
x be Element of subrelstr S, y be Element of R such that
A1: x = y and
A2: x is_minimal_in B;
A3: x in B by A2,WAYBEL_4:56;
assume not y is_minimal_in B;
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;
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;
hence contradiction by A4,A2,WAYBEL_4:56;
end;
theorem Th34: :: PbeSmax:
for R being transitive RelStr, A being StableSet of R,
C being Clique of subrelstr Lower A, a, b being Element of R
st a in A & a in C & b in C holds a = b or b <= a
proof
let R be transitive RelStr, A be StableSet of R,
C be Clique of subrelstr Lower A, a, b be Element of R such that
A1: a in A and
A2: a in C and
A3: b in C;
set ap = subrelstr Lower A;
reconsider a9 = a as Element of ap by A2;
A4: b in the carrier of ap by A3;
reconsider b9 = b as Element of ap by A3;
A5: b9 in Lower A by A4,YELLOW_0:def 15;
A6: C is Clique of R by Th28;
per cases by A5,XBOOLE_0:def 3;
suppose b9 in A;
hence thesis by A1,A2,A3,A6,Th15;
end;
suppose b9 in downarrow A;
then consider c being Element of R such that
A7: b <= c and
A8: c in A by WAYBEL_0:def 15;
per cases;
suppose A9: a <> b;
per cases by A9,A2,A3,Th6;
suppose a9 <= b9;
then a <= b by YELLOW_0:59;
then a <= c by A7,YELLOW_0:def 2;
hence thesis by A8,A7,A1,Def2;
end;
suppose b9 <= a9;
hence thesis by YELLOW_0:59;
end;
end;
suppose a = b;
hence thesis;
end;
end;
end;
theorem Th35: :: PabSmin:
for R being transitive RelStr, A being StableSet of R,
C being Clique of subrelstr Upper A, a, b being Element of R
st a in A & a in C & b in C holds a = b or a <= b
proof
let R be transitive RelStr, A be StableSet of R,
C be Clique of subrelstr Upper A, a, b be Element of R such that
A1: a in A and
A2: a in C and
A3: b in C;
set ap = subrelstr Upper A;
reconsider a9 = a as Element of ap by A2;
A4: b in the carrier of ap by A3;
reconsider b9 = b as Element of ap by A3;
A5: b9 in Upper A by A4,YELLOW_0:def 15;
A6: C is Clique of R by Th28;
per cases by A5,XBOOLE_0:def 3;
suppose b9 in A;
hence thesis by A1,A2,A3,A6,Th15;
end;
suppose b9 in uparrow A;
then consider c being Element of R such that
A7: c <= b and
A8: c in A by WAYBEL_0:def 16;
per cases;
suppose A9: a <> b;
per cases by A9,A2,A3,Th6;
suppose a9 <= b9;
hence thesis by YELLOW_0:59;
end;
suppose b9 <= a9;
then b <= a by YELLOW_0:59;
then c <= a by A7,YELLOW_0:def 2;
hence thesis by A8,A7,A1,Def2;
end;
end;
suppose a = b;
hence thesis;
end;
end;
end;
registration
let R be with_finite_clique# RelStr, S be Subset of R;
cluster subrelstr S -> with_finite_clique#;
coherence 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 P[Nat] means ex c being finite Clique of sS st card c = $1;
A2: for k being Nat st P[k] holds k <= card C proof
let k be Nat;
assume P[k];
then consider c being finite Clique of sS such that
A3: card c = k;
c is finite Clique of R by Th28;
hence thesis by A3,A1;
end;
card {}sS = 0; then
A4: ex k being Nat st P[k];
consider k being Nat such that
A5: P[k] and
A6: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A2,A4);
consider c being finite Clique of sS such that
A7: card c = k by A5;
for D being finite Clique of sS holds card(D) <= card(c) by A7,A6;
hence sS is with_finite_clique#;
end;
end;
registration
let R be with_finite_stability# RelStr, S be Subset of R;
cluster subrelstr S -> with_finite_stability#;
coherence 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#;
defpred P[Nat] means
ex C being finite StableSet of subrelstr S
st card C = $1
& ex B being finite StableSet of subrelstr S st $1 < card(B);
A3: P[0] proof
reconsider C = {}(subrelstr S) as finite StableSet of subrelstr S;
take C;
thus card C = 0;
hence thesis by A2;
end;
A4: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
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);
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;
thus card BB = n+1 by A7;
consider Bb being finite StableSet of subrelstr S such that
A8: card BB < card(Bb) by A2;
take Bb;
thus n+1 < card Bb by A8,A7;
end;
for n being Nat holds P[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;
end;
end;
theorem Th36: :: Pmaxmin:
for R being with_finite_clique# non empty antisymmetric transitive RelStr,
x being Element of R
holds ex y being Element of R st y is_minimal_in [#]R & (y = x or y < x)
proof
let R be with_finite_clique# non empty antisymmetric transitive RelStr,
x be Element of R;
set sx = Lower {x}; set sL = subrelstr sx;
reconsider sL as with_finite_clique# non empty antisymmetric transitive RelStr;
consider y being object such that
A1: y in minimals sL by XBOOLE_0:def 1;
reconsider y as Element of sL by A1;
A2: [#]sL = sx by YELLOW_0:def 15;
then A3: y is_minimal_in sx by A1,Def9;
reconsider y9 = y as Element of R by YELLOW_0:58;
take y9;
sx c= the carrier of sL by YELLOW_0:def 15;
hence y9 is_minimal_in [#]R by A3,Th33,Th24;
per cases;
suppose y9 = x;
hence thesis;
end;
suppose 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 thesis;
end;
end;
theorem :: Pam:
for R being with_finite_clique# antisymmetric transitive RelStr
holds Upper minimals R = [#]R
proof
let R being with_finite_clique# antisymmetric transitive RelStr;
set ap = Upper minimals R; set cR = the carrier of R;
cR c= ap proof
let x be object;
assume A1: x in cR;
then reconsider x9 = x as Element of R;
A2: R is non 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;
per cases by A4;
suppose x9 = y;
hence thesis by A5,XBOOLE_0:def 3;
end;
suppose y < x9;
then y <= x9;
then x in uparrow minimals R by A5,WAYBEL_0:def 16;
hence x in ap by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
theorem Th38: :: Pminmax
for R being with_finite_clique# non empty antisymmetric transitive RelStr,
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 with_finite_clique# non empty antisymmetric transitive RelStr,
x be Element of R;
set ax = Upper {x}; set sU = subrelstr ax;
reconsider sU as with_finite_clique# non empty antisymmetric transitive RelStr;
consider y being object such that
A1: y in maximals sU by XBOOLE_0:def 1;
reconsider y as Element of sU by A1;
A2: [#]sU = ax by YELLOW_0:def 15;
then A3: y is_maximal_in ax by A1,Def10;
reconsider y9 = y as Element of R by YELLOW_0:58;
take y9;
ax c= the carrier of sU by YELLOW_0:def 15;
hence y9 is_maximal_in [#]R by A3,Th32,Th25;
per cases;
suppose y9 = x;
hence thesis;
end;
suppose y9 <> x;
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 thesis;
end;
end;
theorem :: Pbm:
for R being with_finite_clique# antisymmetric transitive RelStr
holds Lower maximals R = [#]R
proof
let P being with_finite_clique# antisymmetric transitive RelStr;
set ap = Lower maximals P; set cP = the carrier of P;
cP c= ap proof
let x be object;
assume A1: x in cP;
then reconsider x9 = x as Element of P;
A2: P is non 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;
per cases by A4;
suppose x9 = y;
hence thesis by A5,XBOOLE_0:def 3;
end;
suppose y > x9;
then x9 <= y;
then x in downarrow maximals P by A5,WAYBEL_0:def 15;
hence x in ap by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
theorem Th40: :: PCAmin:
for R being with_finite_clique# antisymmetric transitive RelStr,
A being StableSet of R
st minimals R c= A holds A = minimals R
proof
let R be with_finite_clique# antisymmetric transitive RelStr,
A be StableSet of R such that
A1: minimals R c= A;
A c= minimals R proof
let x be object;
assume A2: x in A;
then A3: R is non 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;
y in minimals R by A3,A4,Def9;
hence x in minimals R by A1,A2,A6,Def2;
end;
hence A = minimals R by A1;
end;
theorem Th41: :: PCAmax:
for R being with_finite_clique# antisymmetric transitive RelStr,
A being StableSet of R
st maximals R c= A holds A = maximals R
proof
let R be with_finite_clique# antisymmetric transitive RelStr,
A be StableSet of R such that
A1: maximals R c= A;
A c= maximals R proof
let x be object;
assume A2: x in A;
then A3: R is non 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;
y in maximals R by A3,A4,Def10;
hence x in maximals R by A1,A2,A6,Def2;
end;
hence A = maximals R by A1;
end;
theorem Th42: :: Hsubp0:
for R being with_finite_clique# RelStr, S being Subset of R
holds clique# subrelstr S <= clique# R
proof
let R be with_finite_clique# RelStr, S be Subset of R;
set s = subrelstr S;
consider c being finite Clique of s such that
A1: card c = clique# s by Def4;
c is Clique of R by Th28;
hence clique# subrelstr S <= clique# R by Def4,A1;
end;
theorem :: Hsubp1:
for R being with_finite_clique# RelStr, C being Clique of R,
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, C be Clique of R, S be Subset of R
such that
A1: card C = clique# R and
A2: C c= S;
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;
end;
theorem Th44: :: Wsubp0:
for R being with_finite_stability# RelStr, S being Subset of R
holds stability# subrelstr S <= stability# R
proof
let R be with_finite_stability# RelStr, S be Subset of 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;
end;
theorem Th45: :: Wsubp1:
for R being with_finite_stability# RelStr, A being StableSet of R,
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, A be StableSet of R, S be Subset of R
such that
A1: card A = stability# R and
A2: A c= S;
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;
end;
begin :: Partitions into cliques and stable sets
definition
let R be RelStr, P be a_partition of the carrier of R;
attr P is Clique-wise means :Def11:
for x being set st x in P holds x is Clique of R;
end;
registration let R be RelStr;
cluster Clique-wise for a_partition of the carrier of R;
existence
proof set cR = the carrier of R;
per cases;
suppose R is empty;
then reconsider S = {} as a_partition of cR by EQREL_1:45;
take S ;
thus for x being set st x in S holds x is Clique of R;
end;
suppose A1: R is non empty;
take S = SmallestPartition cR;
let z being set;
assume A2: z in S;
S = the set of all {x} where x is Element of cR by A1,EQREL_1:37;
then ex x being Element of cR st z = {x} by A2;
hence z is Clique of R by A1,SUBSET_1:33;
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;
end;
theorem Th46: :: Chpw:
for R being finite RelStr, C being Clique-partition of R
holds card C >= stability# R
proof
let R be finite RelStr, C be Clique-partition of R;
assume A1: card(C) < stability# R;
consider A being StableSet of R such that
A2: card A = stability# R by Def6;
card Segm card C = card C & card Segm card A = card A;
then A3: card C in card A by A1,A2,NAT_1:41;
set cR = the carrier of R;
per cases;
suppose R is empty;
hence contradiction by A1;
end;
suppose A4: R is non empty;
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in A & $2 in C & $1 in D2;
A5: for x being object st x in A ex y being object st y in C & P[x,y] proof
let x be object such that
A6: x in A;
reconsider x9 = x as Element of R by A6;
cR is non empty by A4;
then x9 in cR;
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;
thus thesis by A6,A7,A8;
end;
consider f being Function of A, C such that
A9: for x being object st x in A holds P[x,f.x] from FUNCT_2:sch 1(A5);
consider x,y being object 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;
P[x,f.x] & P[y,f.y] by A10,A11,A9;
then x in f.x & y in f.x by A13;
hence contradiction by A14,A10,A11,A12,Th15;
end;
end;
theorem Th47: :: ACpart1:
for R being with_finite_stability# RelStr, A being StableSet of R,
C being Clique-partition of R st card C = card A
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, A be StableSet of R,
C be Clique-partition of R; assume that
A1: card C = card A;
set cR = the carrier of R;
per cases;
suppose A2: R is empty;
then the carrier of R is empty;
then A3: C = {};
set f = the Function of A, C;
dom f = {} 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;
thus f is bijective by A4;
thus thesis;
end;
suppose A5: R is non empty;
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in A & $2 in C & $1 in D2;
A6: for x being object st x in A ex y being object st y in C & P[x,y] proof
let x be object;
assume A7: x in A;
then reconsider x9 = x as Element of R;
cR is non empty by A5;
then x9 in cR;
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;
thus thesis by A7,A8,A9;
end;
consider f being Function of A, C such that
A10: for x being object st x in A holds P[x,f.x] from FUNCT_2:sch 1(A6);
take f;
A11: f is one-to-one proof
let x1,x2 be object such that
A12: x1 in dom f and
A13: x2 in dom f and
A14: f.x1 = f.x2;
P[x1,f.x1] by A12,A10;
then
A15: x1 in f.x1;
P[x2,f.x2] by A13,A10;
then
A16: x2 in f.x2;
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;
end;
C is finite by A1; then
f is onto by A1,A11,FINSEQ_4:63;
hence f is bijective by A11;
let x be set;
assume x in A;
then P[x,f.x] by A10;
hence x in f.x;
end;
end;
theorem Th48: :: ACpart2:
for R being finite RelStr, A being StableSet of R,
C being Clique-partition of R st card C = card A
for c being set st c in C ex a being Element of A st c /\ A = {a}
proof
let R be finite RelStr, A be StableSet of R,
C be Clique-partition of R such that
A1: card C = card 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 such that
A4: c in C;
rng f = C by A2,FUNCT_2:def 3;
then consider x being object 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;
now
let z be object;
hereby
assume z in c /\ 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;
end;
assume z = a;
hence z in c /\ A by A7,A5,XBOOLE_0:def 4;
end;
hence c /\ A = {a} by TARSKI:def 1;
end;
theorem Th49: :: Glueing lemma:
for R being with_finite_stability# antisymmetric transitive non empty RelStr,
A being StableSet of R,
U being Clique-partition of subrelstr Upper A,
L being Clique-partition of subrelstr Lower A
st card A = stability# R & card U = stability# R & card L = stability# R
ex C being Clique-partition of R st card C = stability# R
proof
let R be with_finite_stability# antisymmetric transitive non empty RelStr,
A be StableSet of R,
U be Clique-partition of subrelstr Upper A,
L be Clique-partition of subrelstr Lower A such that
A1: card A = stability# R and
A2: card U = stability# R and
A3: card L = stability# R;
A4: A is non empty by A1;
set aA = Upper A, bA = Lower A;
set cR = the carrier of R, Pa = subrelstr aA, Pb = subrelstr bA;
A5: aA = the carrier of Pa by YELLOW_0:def 15;
A6: bA = the carrier of Pb by YELLOW_0:def 15;
reconsider Pa = subrelstr Upper A as
with_finite_stability# antisymmetric transitive non empty 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
with_finite_stability# antisymmetric transitive non empty 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 h;
A15: dom h = dom f \/ dom g by LEXBFS:def 2;
A16: C c= bool cR proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in C;
then consider a being object such that
A17: a in dom h and
A18: h.a = x by FUNCT_1:def 3;
A19: h.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= cR by A5,XBOOLE_1:1;
g.a in L by A17,A15,FUNCT_2:5;
then g.a c= cR by A6,XBOOLE_1:1;
then xx c= cR by A18,A19,A20,XBOOLE_1:8;
hence x in bool cR;
end;
A21: union C = cR proof
now let x be object;
hereby assume x in union C;
then consider Y being set such that
A22: x in Y and
A23: Y in C by TARSKI:def 4;
consider a being object such that
A24: a in dom h and
A25: Y = h.a by A23,FUNCT_1:def 3;
A26: x in f.a \/ g.a by A24,A25,A22,A15,LEXBFS:def 2;
per cases by A26,XBOOLE_0:def 3;
suppose A27: x in f.a;
f.a in U by A24,A15,FUNCT_2:5;
then x in aA by A27,A5;
hence x in cR;
end;
suppose A28: x in g.a;
g.a in L by A24,A15,FUNCT_2:5;
then x in bA by A28,A6;
hence x in cR;
end;
end;
assume x in [#]R;
then A29: x in Upper A \/ Lower A by A1,Th23;
per cases by A29,XBOOLE_0:def 3;
suppose x in Upper A;
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 object such that
A32: a in dom f and
A33: Y = f.a by A31,A10,FUNCT_1:def 3;
A34: h.a in rng h by A32,A15,A9,A13,FUNCT_1:3;
h.a = f.a \/ g.a by A32,A15,A9,A13,LEXBFS:def 2;
then x in h.a by A30,A33,XBOOLE_0:def 3;
hence x in union C by A34,TARSKI:def 4;
end;
suppose x in Lower A;
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 object such that
A37: a in dom g and
A38: Y = g.a by A36,A14,FUNCT_1:def 3;
A39: h.a in rng h by A37,A15,A9,A13,FUNCT_1:3;
h.a = f.a \/ g.a by A37,A15,A9,A13,LEXBFS:def 2;
then x in h.a by A35,A38,XBOOLE_0:def 3;
hence x in union C by A39,TARSKI:def 4;
end;
end;
hence thesis by TARSKI:2;
end;
A40: now
let a be Subset of cR;
assume a in C;
then consider x being object such that
A41: x in dom h and
A42: h.x = a by FUNCT_1:def 3;
A43: h.x = f.x \/ g.x by A41,A15,LEXBFS:def 2;
set cfx = f.x, cgx = g.x;
A44: cfx in U by A41,A15,FUNCT_2:5;
then reconsider cfx as Subset of Pa;
A45: cgx in L by A41,A15,FUNCT_2:5;
then reconsider cgx as Subset of Pb;
cfx <> {} by A44;
hence a <> {} by A42,A43;
let b be Subset of cR;
assume b in C;
then consider y being object such that
A46: y in dom h and
A47: h.y = b by FUNCT_1:def 3;
A48: h.y = f.y \/ g.y by A46,A15,LEXBFS:def 2;
set cfy = f.y, cgy = g.y;
A49: cfy in U by A46,A15,FUNCT_2:5;
then reconsider cfy as Subset of Pa;
A50: cgy in L by A46,A15,FUNCT_2:5;
then reconsider cgy as Subset of Pb;
assume A51: a <> 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;
then a /\ b <> {};
then consider z being object 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, cgz = g.z;
per cases by A55,A56,A42,A47,A43,A48,XBOOLE_0:def 3;
suppose z in cfx & z in cfy;
then z in cfx /\ cfy by XBOOLE_0:def 4;
then cfx meets cfy;
hence contradiction by A44,A49,A52,EQREL_1:def 4;
end;
suppose A57: z in cfx & z in cgy;
then A58: z in A by A5,A6,Th22;
A59: z in f.z by A57,A5,A6,Th22,A8;
A60: cfz in U by A57,A5,A6,Th22,FUNCT_2:5;
then reconsider cfz as Subset of Pa;
z in cfx /\ cfz by A57,A59,XBOOLE_0:def 4;
then cfz meets cfx;
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: cgz in L by A57,A5,A6,Th22,FUNCT_2:5;
then reconsider cgz as Subset of Pb;
z in cgz /\ cgy by A57,A62,XBOOLE_0:def 4;
then cgz meets cgy;
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;
end;
suppose A64: z in cgx & z in cfy;
then A65: z in A by A5,A6,Th22;
A66: z in f.z by A64,A5,A6,Th22,A8;
A67: cfz in U by A64,A5,A6,Th22,FUNCT_2:5;
then reconsider cfz as Subset of Pa;
z in cfy /\ cfz by A64,A66,XBOOLE_0:def 4;
then cfz meets cfy;
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: cgz in L by A64,A5,A6,Th22,FUNCT_2:5;
then reconsider cgz as Subset of Pb;
z in cgz /\ cgx by A64,A69,XBOOLE_0:def 4;
then cgz meets cgx;
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;
end;
suppose z in cgx & z in cgy;
then z in cgx /\ cgy by XBOOLE_0:def 4;
then cgx meets cgy;
hence contradiction by A45,A50,A53,EQREL_1:def 4;
end;
end;
A71: for x being set st x in C holds x is Clique of R
proof
let c be set;
assume c in C;
then consider x being object such that
A72: x in dom h and
A73: c = h.x by FUNCT_1:def 3;
A74: c = f.x \/ g.x by A72,A73,A15,LEXBFS:def 2;
set cf = f.x, cg = g.x;
cf in U by A72,A15,FUNCT_2:5;
then
A75: cf is Clique of Pa by Def11;
then A76: cf is Clique of R by Th28;
cg in L by A72,A15,FUNCT_2:5;
then
A77: cg is Clique of Pb by Def11;
then A78: cg is Clique of R by Th28;
then reconsider c9 = c as Subset of R by A74,A76,XBOOLE_1:8;
now let a, b being Element of R such that
A79: a in c9 and
A80: b in c9 and
A81: a <> b;
A82: x in cf by A72,A15,A8;
A83: x in cg by A72,A15,A12;
reconsider x as Element of R by A72,A15,A9,A13;
per cases by A79,A80,A74,XBOOLE_0:def 3;
suppose a in f.x & b in f.x;
hence a <= b or b <= a by A76,A81,Th6;
end;
suppose A84: a in f.x & b in g.x;
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;
end;
suppose A86: a in g.x & b in f.x;
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;
end;
suppose a in g.x & b in g.x;
hence a <= b or b <= a by A78,A81,Th6;
end;
end;
hence c is Clique of R by Th6;
end;
A88: h is one-to-one proof
let x1,x2 be object such that
A89: x1 in dom h and
A90: x2 in dom h and
A91: h.x1 = h.x2;
A92: h.x1 is Clique of R by A71,A89,FUNCT_1:3;
A93: h.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 h.x1 by A93,XBOOLE_0:def 3;
A95: h.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 h.x2 by A95,XBOOLE_0:def 3;
hence x1 = x2 by A15,A89,A90,A91,A92,A94,Th15;
end;
reconsider C as Clique-partition of R
by A16,A21,A40,A71,Def11,EQREL_1:def 4;
take C;
card C = card h by A88,PRE_POLY:19
.= card A by A15,A9,A13,CARD_1:62;
hence card C = stability# R by A1;
end;
definition
let R be RelStr, P be a_partition of the carrier of R;
attr P is StableSet-wise means
:Def12:
for x being set st x in P holds x is StableSet of R;
end;
registration
let R be RelStr;
cluster StableSet-wise for a_partition of the carrier of R;
existence
proof set cR = the carrier of R;
per cases;
suppose R is empty;
then reconsider S = {} as a_partition of cR by EQREL_1:45;
take S;
let x be set;
thus thesis;
end;
suppose A1: R is non empty;
then reconsider RR = R as non empty RelStr;
take S = SmallestPartition cR;
let z being set;
assume A2: z in S;
S = the set of all {x} where x is Element of cR 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;
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;
end;
theorem :: ColClique:
for R being finite RelStr, C being Coloring of R holds card C >= clique# R
proof
let R be finite RelStr, C be Coloring of R;
assume A1: card(C) < clique# R;
consider A being Clique of R such that
A2: card A = clique# R by Def4;
card Segm card C = card C & card Segm card A = card A;
then A3: card C in card A by A1,A2,NAT_1:41;
set cR = the carrier of R;
per cases;
suppose R is empty;
hence contradiction by A1;
end;
suppose A4: R is non empty;
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in A & $2 in C & $1 in D2;
A5: for x being object st x in A ex y being object st y in C & P[x,y] proof
let x be object such that
A6: x in A;
reconsider x9 = x as Element of R by A6;
cR is non empty by A4;
then x9 in cR;
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;
thus thesis by A6,A7,A8;
end;
consider f being Function of A, C such that
A9: for x being object st x in A holds P[x,f.x] from FUNCT_2:sch 1(A5);
consider x,y being object 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;
P[x,f.x] & P[y,f.y] by A10,A11,A9;
then x in f.x & y in f.x by A13;
hence contradiction by A14,A10,A11,A12,Th15;
end;
end;
begin :: Dilworth's theorem and a dual
:: There seems to be little theory of antisymmetric transitive relations.
:: Posets are required to be reflexive and antisymmetric while
:: strict posets to be irreflexive and asymmetric (and both are
:: required to be transitive.) Since asymmetric implies antisymmetric,
:: it seems that the common ground would be antisymmetric and transitive
:: relations.
::$N Dilworth's Decomposition Theorem
::$L https://en.wikipedia.org/wiki/Dilworth's_theorem Dilworth's Decomposition Theorem
theorem Th51: :: Dilworth: Finite case
for R being finite antisymmetric transitive RelStr
ex C being Clique-partition of R st card(C) = stability# R
proof
defpred P[Nat] means
for P being finite antisymmetric transitive RelStr
st card(P) = $1 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 P[k] holds P[n] proof
let n be Nat; assume
A2: for k being Nat st k < n holds P[k];
let P be finite antisymmetric transitive RelStr; assume
A3: card(P) = n;
set wP = stability# P;
per cases;
suppose A4: n = 0;
then P is empty by A3;
then reconsider C = {} as Clique-partition of P by EQREL_1:45;
take C;
P is empty by A3,A4;
hence card(C) = stability# P;
end;
suppose A5: n > 0;
per cases;
suppose ex A being StableSet of P st card(A) = stability# P &
A <> minimals(P) & A <> maximals(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, bA = Lower A;
set cP = the carrier of P, Pa = subrelstr aA, Pb = subrelstr bA;
reconsider PP = P as finite non empty antisymmetric transitive RelStr
by A5,A3;
A9: aA = the carrier of Pa by YELLOW_0:def 15;
A10: bA = the carrier of Pb by YELLOW_0:def 15;
not minimals PP c= aA by A7,Th40,Th26;
then consider mi being object such that
A11: mi in minimals P and
A12: not mi in aA;
not maximals PP c= bA by A8,Th41,Th27;
then consider ma being object such that
A13: ma in maximals P and
A14: not ma in bA;
reconsider Pa as finite antisymmetric transitive RelStr;
mi in cP by A11;
then aA c< cP by A12;
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 = wP by A6,Th45,XBOOLE_1:7;
reconsider Pb as finite antisymmetric transitive RelStr;
ma in cP by A13;
then bA c< cP by A14;
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 = wP 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;
thus card(C) = stability# P by A18;
end;
suppose A19: for A being StableSet of P st card(A) = stability# P
holds A = minimals(P) or A = maximals(P);
consider S being StableSet of P such that
A20: card(S) = stability# P by Def6;
reconsider PP = P as finite non empty antisymmetric transitive RelStr
by A5,A3;
set cR = the carrier of PP;
set a = the Element of minimals(P);
A21: a in minimals(PP);
then reconsider a 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 = cP \ Cn;
A25: cP = cP9 \/ Cn by XBOOLE_1:45;
A26: cP9 misses {a,b} by XBOOLE_1:79;
then A27: cP \ cP9 = {a,b} by A25,XBOOLE_1:88;
reconsider cP9 as Subset of cR;
set P9 = subrelstr cP9;
A28: cP9 = the carrier of P9 by YELLOW_0:def 15;
A29: card cP9= card P9 by YELLOW_0:def 15;
card cP9 = card cP - card {a,b} by CARD_2:44;
then consider C being Clique-partition of P9 such that
A30: card(C) = stability# P9 by A2,A3,A29,XREAL_1:44;
A31: not {a,b} in C proof
assume :: works through typing: Subset-Family -> Subset bool ...
A32: {a,b} in C;
a in {a,b} by TARSKI:def 2;
hence contradiction by A26,A28,A32,ZFMISC_1:49;
end;
set wP = stability# PP; set wP1 = wP - 1;
0+1 <= wP by NAT_1:13;
then 0+1-1 <= wP-1 by XREAL_1:9;
then wP1 in NAT by INT_1:3;
then reconsider wP1 as Nat;
set S9 = S /\ cP9;
S /\ cP = S by XBOOLE_1:28;
then A33: S9 = S \ {a,b} by XBOOLE_1:49;
A34: {a,b} = {a} \/ {b} by ENUMSET1:1;
reconsider S9 as StableSet of P9 by Th31;
A35: card S9 = wP1 proof
per cases by A19,A20;
suppose A36: S = minimals(P);
S9 = S \ {a} proof
per cases;
suppose a = b;
hence S9 = S \ {a} by A33,ENUMSET1:29;
end;
suppose A37: a <> b;
now
assume b in minimals(PP);
then b is_minimal_in [#]PP by Def9;
hence contradiction by A37,A23,WAYBEL_4:56;
end;
hence S9 = S \ {a} by A33,A34,A36,Th1;
end;
end;
hence card S9 = card S - card {a} by A36,EULER_1:4
.= wP1 by A20,CARD_1:30;
end;
suppose A38: S = maximals(PP);
A39: S9 = S \ {b} proof
per cases;
suppose a = b;
hence S9 = S \ {b} by A33,ENUMSET1:29;
end;
suppose A40: a <> b;
now
assume a in maximals(PP);
then a is_maximal_in [#]PP by Def10;
hence contradiction by A40,A23,WAYBEL_4:55;
end;
hence S9 = S \ {b} by A33,A34,A38,Th1;
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;
end;
end;
for T being StableSet of P9 holds card(T) <= card(S9) proof
let T be StableSet of P9;
assume card(T) > card(S9);
then card T >= card S9 + 1 by NAT_1:13;
then consider V being StableSet of P9 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;
end;
then A42: stability# P9 + 1 = wP - 1 + 1 by A35,Def6 .= wP;
set CC = C \/ {{a,b}};
cP9 <> cP by A27,XBOOLE_1:37;
then
A43: cP9 c< cP;
now :: Cliques in CC
let x be set;
assume A44: x in CC;
per cases by A44,XBOOLE_0:def 3;
suppose x in C;
then x is Clique of P9 by Def11;
hence x is Clique of P by Th28;
end;
suppose x in {{a,b}};
then A45: x = {a,b} by TARSKI:def 1;
per cases;
suppose a = b;
then x = {a} by A45,ENUMSET1:29;
hence x is Clique of P;
end;
suppose a <> b;
then a <= b by A23;
hence x is Clique of P by A45,Th8;
end;
end;
end;
then reconsider CC as Clique-partition of P by A27,A28,Th4,Def11,A43;
take CC;
thus card(CC) = stability# P by A30,A42,A31,CARD_2:41;
end;
end;
end;
A46: for n being Nat holds P[n] from NAT_1:sch 4(A1);
let R be finite antisymmetric transitive RelStr;
card R = card R;
hence thesis by A46;
end;
definition
let R be with_finite_stability# non empty RelStr, C be Subset of R;
attr C is strong-chain means
for S being finite non empty 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;
registration let R be with_finite_stability# non empty RelStr;
cluster strong-chain -> clique for Subset of R;
coherence
proof
let C be Subset of R;
assume A1: C is strong-chain;
now
let a, b be Element of R such that
A2: a in C and
A3: b in C and
A4: a <> b;
set S = {a,b};
reconsider S as finite non empty 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;
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;
end;
hence C is clique by Th6;
end;
end;
registration
let R be with_finite_stability# antisymmetric transitive non empty RelStr;
cluster 1-element -> strong-chain for Subset of R;
coherence
proof
let C be Subset of R;
assume C is 1-element;
then consider x being object such that
A1: C = {x} by ZFMISC_1:131;
let S be finite non empty Subset of R;
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;
thus card P <= stability# R by A2,Th44;
per cases;
suppose x in S;
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;
thus c in P by A5;
thus S /\ C c= c proof
let a be object;
assume a in S /\ C;
then a in C by XBOOLE_0:def 4;
hence thesis by A4,A1,TARSKI:def 1;
end;
let d be set such that
A6: d in P and
A7: d <> c;
assume C /\ d <> {};
then consider a being object such that
A8: a in C /\ d by XBOOLE_0:def 1;
reconsider d, 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;
hence contradiction by A6,A5,A7,EQREL_1:def 4;
end;
suppose A9: not x in S;
set c = the Element of P;
take c;
thus c in P;
C misses S by A9,A1,ZFMISC_1:50;
then S /\ C = {};
hence S /\ C c= c;
let d be set such that
A10: d in P and d <> c;
not x in d by A9,A3,A10;
then C misses d by A1,ZFMISC_1:50;
hence C /\ d = {};
end;
end;
end;
theorem Th52: :: Maxsc:
for R being with_finite_stability# non empty antisymmetric transitive RelStr
ex S being non empty Subset of R
st S is strong-chain &
not ex D being Subset of R st D is strong-chain & S c< D
proof
let R be with_finite_stability# non empty antisymmetric transitive RelStr;
set E = { C where C is Subset of R: C is strong-chain };
set x = the Element of R;
A1: {x} in E;
now :: premise of maximal principle
let Z be set such that
A2: Z c= E and
A3: Z is c=-linear;
set Y = union Z;
take Y;
now
let B be set;
assume B in Z;
then B in E by A2;
then ex C being Subset of R st C = B & C is strong-chain;
hence B c= the carrier of R;
end;
then reconsider Y9 = Y as Subset of R by ZFMISC_1:76;
Y9 is strong-chain proof
let S be finite non empty Subset of R;
set F = S /\ Y;
per cases;
suppose A4: F is empty;
consider p being Clique-partition of subrelstr S such that
A5: card p = stability# subrelstr S by Th51;
take p;
thus card p <= stability# R by Th44,A5;
set c = the Element of p;
take c;
thus c in p;
thus S /\ Y9 c= c by A4;
let d be set such that
A6: d in p and d <> c;
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,26;
end;
suppose A7: F is non empty;
then A8: Z is non empty by ZFMISC_1:2;
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in F & $2 in Z & $1 in D2;
A9: for x being object st x in F ex y being object st y in Z & P[x,y] proof
let x be object;
assume A10: x in F;
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;
thus thesis by A12,A10,A11;
end;
consider f being Function of F, Z such that
A13: for x being object st x in F holds P[x,f.x] from FUNCT_2:sch 1(A9);
set rf = rng f;
rf c= Z & Z is c=-linear implies rf is c=-linear;
then consider m being set such that
A14: m in rf and
A15: for C being set st C in rf holds C c= m
by A3,A7,A8,FINSET_1:12,RELAT_1:def 19;
rf c= Z by RELAT_1:def 19;
then m in Z by A14;
then m in E by A2;
then consider C being Subset of R such that
A16: m = C and
A17: C is strong-chain;
A18: F c= C proof
let x be object;
assume A19: x in F;
then P[x,f.x] by A13;
then A20: x in f.x;
f.x c= C by A16,A15,A19,A8,FUNCT_2:4;
hence x in C by A20;
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;
take p;
thus card p <= stability# R by A21;
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;
thus c in p by A23;
thus S /\ Y9 c= c proof
let x be object;
assume x in S /\ Y9;
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;
end;
let d be set such that
A26: d in p and
A27: d <> c;
assume Y9 /\ d <> {};
then consider x being object 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 F 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;
end;
end;
hence Y in E;
let X1 be set such that
A31: X1 in Z;
thus X1 c= Y by A31,ZFMISC_1:74;
end;
then consider Y being set such that
A32: Y in E and
A33: for Z being set st Z in E & 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;
thus S is strong-chain by A35;
let D be Subset of R such that
A36: D is strong-chain and
A37: S c< D;
A38: D in E by A36;
D <> S & S c= D by A37;
hence contradiction by A34,A38,A33;
end;
theorem :: Dilworth: General case
for R being with_finite_stability# antisymmetric transitive RelStr
ex C being Clique-partition of R st card C = stability# R
proof
let R be with_finite_stability# antisymmetric transitive RelStr;
per cases;
suppose R is finite;
hence thesis by Th51;
end;
suppose A1: R is infinite;
defpred P[Nat] means
for P being with_finite_stability# non empty antisymmetric transitive RelStr
st stability# P = $1
ex C being Clique-partition of P st card(C) = stability# P;
A2: P[0];
A3: for k be Nat st P[k] holds P[k + 1] proof
let k be Nat;
assume A4: P[k];
let P be with_finite_stability# non empty antisymmetric transitive RelStr;
assume A5: stability# P = k+1;
consider C being non empty Subset of P such that
A6: C is strong-chain and
A7: not ex D being Subset of P st D is strong-chain & C c< D by Th52;
set cP = the carrier of P;
per cases;
suppose A8: C = cP; :: real base case
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;
A9: cP = [#]P;
thus card Cp = 1 by CARD_1:30
.= stability# P by A9,A6,A8,Th20;
end;
suppose C <> cP;
then A10: C c< cP;
set cP9 = cP \ C;
A11: cP \ cP9 = cP /\ C by XBOOLE_1:48
.= C by XBOOLE_1:28;
reconsider cP9 as Subset of P;
cP9 <> {} by A10,XBOOLE_1:105;
then reconsider P9 = subrelstr cP9
as with_finite_stability# non empty antisymmetric transitive 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;
consider A being finite StableSet of P9 such that
A16: card(A) = stability# P9 by Def6;
reconsider A9 = A as finite non empty StableSet of P by A16,Th30;
defpred R[set, set, set] means
for c being set st c in $2 holds not $1 /\ $3 c= c or
ex d being set st d in $2 & d <> c & $3 /\ d <> {};
defpred Q[finite Subset of P,set] means
for p being Clique-partition of subrelstr $1
st card p <= stability# P holds R[$1,p,$2];
defpred P[object,object] means
ex S being finite non empty Subset of P
st $2 = S & $1 in S & Q[S, C\/{$1}];
A17: for x being object st x in A ex y being object st P[x,y] proof
let a be object;
assume A18: a in A;
A c= cP by A12,XBOOLE_1:1;
then {a} c= cP by A18,ZFMISC_1:31;
then reconsider Ca = C \/ {a} as Subset of P by XBOOLE_1:8;
now
assume A19: Ca is strong-chain;
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;
hence contradiction by A19,A7;
end;
then consider S being finite non empty Subset of P such that
A22: Q[S,Ca];
take S;
take S;
thus S = S;
now
assume A23: not a in S;
A24: S /\ C c= S /\ Ca proof
let x be object;
assume x in S /\ C;
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;
end;
S /\ Ca c= S /\ C proof
let x be object;
assume A25: x in S /\ Ca;
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;
end;
then A27: S /\ C = S /\ Ca by A24;
consider p being Clique-partition of subrelstr S such that
A28: card p <= stability# P and
A29: not R[S,p,C] by A6;
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 such that
A33: d in p and
A34: d <> c;
now
assume Ca /\ d <> {};
then consider x being object 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;
per cases by A36,XBOOLE_0:def 3;
suppose x in C;
then x in C /\ d by A37,XBOOLE_0:def 4;
hence contradiction by A33,A34,A32;
end;
suppose x in {a};
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;
end;
end;
hence Ca /\ d = {};
end;
hence contradiction by A30,A31,A28,A27,A22;
end;
hence a in S;
thus thesis by A22;
end;
consider f being Function such that
A38: dom f = A and
A39: for x being object st x in A holds P[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;
assume x in rng f;
then consider a being object such that
A42: a in dom f and
A43: x = f.a by FUNCT_1:def 3;
P[a,f.a] by A38,A42,A39;
then consider S being finite non empty Subset of P such that
A44: f.a = S and a in f.a & Q[S, C \/ {a}];
thus x is finite by A44,A43;
end;
A45: SS c= cP proof
let x be object;
assume x in SS;
then consider y being set such that
A46: x in y and
A47: y in rng f by TARSKI:def 4;
consider a being object such that
A48: a in dom f and
A49: y = f.a by A47,FUNCT_1:def 3;
P[a,f.a] by A38,A48,A39;
then consider S being finite non empty Subset of P such that
A50: f.a = S and a in f.a & Q[S, C \/ {a}];
thus x in cP by A46,A49,A50;
end;
A51: A9 c= SS proof
let x be object;
assume A52: x in A9;
then P[x,f.x] by A39;
then consider S being finite non empty Subset of P such that
f.x = S and
A53: x in f.x and Q[S, C \/ {x}];
f.x in rng f by A52,A38,FUNCT_1:3;
hence x in SS by A53,TARSKI:def 4;
end;
then reconsider SS as finite non empty Subset of P
by A41,A40,A45,FINSET_1:7;
set SSp = subrelstr SS;
A54: SS = the carrier of SSp by YELLOW_0:def 15;
consider p being Clique-partition of SSp such that
A55: card p <= stability# P and
A56: not R[SS,p,C] by A6;
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 as Element of p by A57;
A9 = A9 /\ SS by A51,XBOOLE_1:28;
then reconsider A = A9 as finite non empty StableSet of SSp by Th31;
A60: stability# SSp >= card A by Def6;
card p >= stability# SSp 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;
P[a,f.a] by A39;
then consider S being finite non empty Subset of P such that
A63: f.a = S and
A64: a in f.a and
A65: Q[S, C \/ {a}];
deffunc F(set) = $1 /\ S;
defpred P[set] means $1 meets S;
set Sp = { F(e) where e is Element of p: P[e]};
A66: S c= SS proof
let x be object;
assume A67: x in S;
S in rng f by A63,A38,FUNCT_1:3;
hence x in SS by A67,TARSKI:def 4;
end;
then reconsider Sp 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;
assume x in Sp;
then consider e being Element of p such that
A68: x = e /\ S and e meets S;
e is Clique of SSp by Def11;
then e is Clique of P by Th28;
hence x is Clique of subrelstr S by A68,Th29;
end;
then reconsider Sp as Clique-partition of subrelstr S
by Def11,YELLOW_0:def 15;
A69: Sp = { F(e) where e is Element of p: P[e]};
A70: card Sp <= card p from FraenkelFinCard1(A69);
set cc = c /\ S;
c meets S by A62,A63,A64,XBOOLE_0:3; then
A71: cc in Sp;
S /\ (C \/ {a}) c= cc proof
let x be object;
assume A72: x in S /\ (C \/ {a});
then A73: x in S by XBOOLE_0:def 4;
A74: x in C \/ {a} by A72,XBOOLE_0:def 4;
per cases by A74,XBOOLE_0:def 3;
suppose x in C;
then x in SS /\ C by A73,A66,XBOOLE_0:def 4;
hence x in cc by A73,A58,XBOOLE_0:def 4;
end;
suppose x in {a};
then x = a by TARSKI:def 1;
hence x in cc by A62,A63,A64,XBOOLE_0:def 4;
end;
end;
then consider d being set such that
A75: d in Sp and
A76: d <> cc 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 object 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;
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
per cases;
suppose A84: A /\ C = {};
A c= cP9 proof
let x be object;
assume A85: x in A;
then not x in C by A84,XBOOLE_0:def 4;
hence x in cP9 by A85,XBOOLE_0:def 5;
end;
hence thesis by A5,A14,A82,Th45;
end;
suppose A /\ C <> {};
then consider x being object 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 = A9 \/ {x} by XBOOLE_1:45;
x in {x} by TARSKI:def 1;
then not x in A9 by XBOOLE_0:def 5;
then A90: card A = card A9 + 1 by A89,CARD_2:41;
A91: A9 c= A by XBOOLE_1:36;
A9 c= cP9 proof
let xx be object;
assume A92: xx in A9;
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;
end; then
A94: A9 c= A /\ cP9 by A91,XBOOLE_1:19;
A /\ cP9 c= A9 proof
let xx be object;
assume A95: xx in A /\ cP9;
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 A9 by A96,XBOOLE_0:def 5;
end;
then A9 = A /\ cP9 by A94;
then reconsider A9 as StableSet of P9 by Th31;
stability# P9 >= card A9 by Def6;
hence thesis by A90,A82,A5,A81,XXREAL_0:1;
end;
end;
then consider Cp9 being Clique-partition of P9 such that
A97: card(Cp9) = stability# P9 by A4;
set Cp = Cp9 \/ { cP \ cP9 };
A98: Cp9 is finite by A97;
cP9 <> cP by A11,XBOOLE_1:37;
then
A99: cP9 c< cP;
then reconsider Cp as a_partition of cP by A12,Th4;
now :: chains in Cp;
let x be set;
assume A100: x in Cp;
per cases by A100,XBOOLE_0:def 3;
suppose x in Cp9;
then x is Clique of P9 by Def11;
hence x is Clique of P by Th28;
end;
suppose x in { cP \ cP9 };
hence x is Clique of P by A6,A11,TARSKI:def 1;
end;
end;
then reconsider Cp as Clique-partition of P by Def11;
take Cp;
not cP \ cP9 in Cp9 proof
assume not thesis;
then cP c= cP9 \/ cP9 by A12,XBOOLE_1:44;
hence contradiction by A99,XBOOLE_1:60;
end;
hence card Cp = stability# P by A5,A83,A97,A98,CARD_2:41;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
end;
theorem :: A dual of Dilworth's theorem
for R being with_finite_clique# antisymmetric transitive RelStr
ex A being Coloring of R st card A = clique# R
proof
let R be with_finite_clique# antisymmetric transitive RelStr;
defpred P[Nat] means
for P being with_finite_clique# antisymmetric transitive RelStr
st clique# P = $1 ex A being Coloring of P st card A = clique# P;
A1: P[0] proof
let P be with_finite_clique# antisymmetric transitive RelStr;
assume A2: clique# P = 0;
then P is empty;
then reconsider C = {} as Coloring of P by EQREL_1:45;
take C;
thus card(C) = clique# P by A2;
end;
A3: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
assume A4: P[n];
let P be with_finite_clique# antisymmetric transitive RelStr;
assume A5: clique# P = n+1;
then A6: P is non empty;
reconsider PP = P
as with_finite_clique# non empty antisymmetric transitive RelStr by A5;
set M = maximals(PP);
set cP = the carrier of P;
set cPM = cP \ M;
reconsider cPM as Subset of P;
set PM = subrelstr cPM;
A7: cPM = the carrier of PM by YELLOW_0:def 15;
reconsider PM as with_finite_clique# antisymmetric transitive 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 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 /\ M = {m} proof
thus C /\ M c= {m} proof
let a be object;
assume A16: a in C /\ M;
then A17: a in C by XBOOLE_0:def 4;
A18: a in M 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
assume A20: a <> m;
not m < a9 by A17,A14,WAYBEL_4:55;
then not m <= a9 by A20;
then a9 <= m by A12,A17,A20,Th6;
then a9 < m by A20;
hence contradiction by A19,A12,WAYBEL_4:55;
end;
hence a in {m} by TARSKI:def 1;
end;
thus {m} c= C /\ M proof
let a be object;
assume a in {m};
then A21: a = m by TARSKI:def 1;
now
assume A22: not a in M;
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
per cases;
suppose m = y;
hence Cm is finite Clique of P by A12,ZFMISC_1:40;
end;
suppose m <> y;
then m <= y by A24;
hence Cm is finite Clique of P by A14,Th11;
end;
end;
then reconsider Cm 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;
end;
hence a in C /\ M by A21,A12,XBOOLE_0:def 4;
end;
end;
A25: cC = C /\ cP \ C /\ M by XBOOLE_1:50;
C /\ cP = 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
assume A29: clique# PM = n+1;
then A30: Ca <> {} by A8;
A31:PM is non 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
per cases;
suppose x9 = y;
hence Cb is finite Clique of P by A32,A9,ZFMISC_1:40;
end;
suppose x9 <> y;
then x9 <= y by A36;
hence Cb is finite Clique of P by A34,Th32,A9,Th11;
end;
end;
then reconsider Cb as finite Clique of P;
y in M 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;
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 \/ {M};
A39: cP = cPM \/ M by XBOOLE_1:45;
{M} is a_partition of M by EQREL_1:39;
then
A40: A is a_partition of cP by A39,A7,Th3,XBOOLE_1:79;
now let x be set;
assume A41: x in A;
per cases by A41,XBOOLE_0:def 3;
suppose x in Aa;
then x is StableSet of PM by Def12;
hence x is StableSet of P by Th30;
end;
suppose x in {M};
hence x is StableSet of P by TARSKI:def 1;
end;
end;
then reconsider A as Coloring of P by A40,Def12;
take A;
not M in Ab by A7,XBOOLE_1:38;
hence card A = clique# P by A5,A38,CARD_2:41;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A3);
hence ex A being Coloring of R st card(A) = clique# R;
end;
begin :: Erdos-Szekeres theorem
::$N Erdos-Szekeres Theorem
::$L https://en.wikipedia.org/wiki/ErdosâSzekeres_theorem Erdos-Szekeres Theorem
theorem Th55: :: CSR
for R being finite antisymmetric transitive RelStr, r, s being Nat
st card R = r*s+1
holds (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 antisymmetric transitive RelStr, r, s be Nat such 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;
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 f = card p by FINSEQ_1:93;
A8: dom f = Seg len f by FINSEQ_1:def 3;
set f = canFS p;
A9: rng f = p by FUNCT_2:def 3;
then reconsider f as FinSequence of bool cR by FINSEQ_1:def 4;
now
let d,e be Nat such that
A10: d in dom f and
A11: e in dom f and
A12: d<>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 cR 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;
end;
then
A15: card union rng f = Sum Card f by INT_5:48;
reconsider n9 = r as Element of NAT by ORDINAL1:def 12;
reconsider h = wR |-> n9 as Element of wR-tuples_on NAT;
A16: Sum h = wR*r by RVSUM_1:80;
dom f = dom Card f by CARD_3:def 2;
then
len Card f = wR by A7,A4,FINSEQ_3:29;
then
reconsider Cf = Card f as Element of wR-tuples_on NAT by FINSEQ_2:92;
now
let j be Nat such that
A19: j in Seg wR;
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;
end;
then
A22: Sum Cf <= Sum h by RVSUM_1:82;
wR*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;
end;
:: In a sequence of n^2+1 (distinct) real numbers there is a monotone
:: subsequence of length at least n+1.
:: Let F be the sequence. Define a RelStr with the carrier equal F (a set
:: of ordered pairs) and the relation defined as: if a = [i,F.i] in F and
:: b = [j,F.j] in F, for some i and j, then a < b iff i < j & F.i < F.j.
:: The relation is asymmetric and transitive.
:: Considered defining FinSubsequence of f but have given up.
:: There is not much gain from having FinSubsequence of f instead of
:: FinSubsequence st g c= f
::$N Ascending or Descending Sequences
::$L https://en.wikipedia.org/wiki/Sequence Sequences
theorem
for f being real-valued FinSequence, n being Nat
st card f = n^2+1 & f is one-to-one
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, n be Nat such that
A1: card f = n^2+1 and
A2: f is one-to-one;
set cP = f;
defpred P[object,object] means
ex i,j being Nat, r, s being Real
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 object holds [x,y] in iP iff x in f & y in f & P[x,y]
from RELSET_1:sch 1;
set P = RelStr (# cP, iP #);
A4: dom f = Seg len f by FINSEQ_1:def 3;
A5: P is antisymmetric proof
let x, y be object such that
x in the carrier of P and y in the carrier of P and
A6: [x,y] in the InternalRel of P and
A7: [y,x] in the InternalRel of P;
consider i,j being Nat, r, s being Real 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 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;
end;
P is transitive proof
let x, y, z be object such that
A14: x in the carrier of P and y in the carrier of P and
A15: z in the carrier of P and
A16: [x,y] in the InternalRel of P and
A17: [y,z] in the InternalRel of P;
consider ix,jy being Nat, rx, sy being Real 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 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 P by A18,A22,A14,A15,A3;
end;
then reconsider P as finite antisymmetric transitive RelStr by A5;
A24: card P = card f;
per cases by A24,A1,Th55;
suppose ex C being Clique of P st card C >= n+1;
then consider C being Clique of P such that
A25: card C >= n+1;
set g = C;
reconsider g as Subset of f;
reconsider g as Function;
dom g c= Seg len f proof
let x be object;
assume x in dom g;
then consider y being object such that
A26: [x,y] in g by XTUPLE_0:def 12;
x in dom f by A26,XTUPLE_0:def 12;
hence thesis by FINSEQ_1:def 3;
end;
then reconsider g as FinSubsequence by FINSEQ_1:def 12;
reconsider g as real-valued FinSubsequence;
take g;
thus g c= f;
thus card g >= n+1 by A25;
g is increasing proof
let e1, e2 be ExtReal such that
A27: e1 in dom g and
A28: e2 in dom g and
A29: e1 < e2;
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;
per cases by A30,A31,A32,Th6;
suppose p1 <= p2;
then [p1,p2] in iP;
then consider i,j being Nat, r, s being Real 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;
end;
suppose p2 <= p1;
then [p2,p1] in iP;
then consider i,j being Nat, r, s being Real 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;
end;
end;
hence thesis;
end;
suppose ex A being StableSet of P st card A >= n+1;
then consider A being StableSet of P such that
A39: card A >= n+1;
set g = A;
reconsider g as Subset of f;
reconsider g as Function;
A40: dom g c= Seg len f proof
let x be object;
assume x in dom g;
then consider y being object such that
A41: [x,y] in g by XTUPLE_0:def 12;
x in dom f by A41,XTUPLE_0:def 12;
hence thesis by FINSEQ_1:def 3;
end;
then reconsider g as FinSubsequence by FINSEQ_1:def 12;
reconsider g as real-valued FinSubsequence;
take g;
thus g c= f;
thus card g >= n+1 by A39;
g is decreasing proof
let e1, e2 be ExtReal such that
A42: e1 in dom g and
A43: e2 in dom g and
A44: e1 < 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;
reconsider i = e1, j = e2 as Nat by A42,A43;
reconsider r = g.e1, s = g.e2 as Real;
A49: p1 = [i,r] & p2 = [j,s];
per cases by A48,XXREAL_0:1;
suppose g.e1 < g.e2;
then [p1,p2] in iP by A45,A3,A44,A49;
then p1 <= p2;
hence g.e1 > g.e2 by A45,A46,A47,Def2;
end;
suppose g.e1 > g.e2;
hence thesis;
end;
end;
hence thesis;
end;
end;