:: Dilworth's Decomposition Theorem for Posets
:: by Piotr Rudnicki
::
:: Received September 17, 2009
:: Copyright (c) 2009 Association of Mizar Users
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,
XREAL_0, DILWORTH;
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, NAT_1, EQREL_1,
FUNCT_1, FUNCT_2, NUMBERS, GROUP_1, XREAL_0, XXREAL_0, YELLOW_0,
XCMPLX_0, ZFMISC_1, LEXBFS, ORDINAL1, FINSEQ_1, SQUARE_1, UPROOTS,
RVSUM_1, INT_5, FINSEQ_2, VALUED_0, GROUP_10, RAMSEY_1, DOMAIN_1;
constructors DOMAIN_1, SETFAM_1, ORDERS_3, LEXBFS, WAYBEL_4, SQUARE_1,
UPROOTS, WSIERP_1, PROB_3, INT_5, SEQ_1, RAMSEY_1, RELSET_1, BINOP_2;
registrations STRUCT_0, MEMBERED, XXREAL_0, RELSET_1, CARD_1, YELLOW_0,
XREAL_0, FINSET_1, XBOOLE_0, ORDERS_3, NAT_1, INT_1, YELLOW_2, EQREL_1,
FINSEQ_1, FUNCT_1, SUBSET_1, ORDINAL1, PEPIN, RVSUM_1, UPROOTS, FUNCT_2,
FINSEQ_2, NUMBERS, PNPROC_1, RELAT_1, VALUED_0, ZFMISC_1, ORDERS_2;
requirements ARITHM, SUBSET, BOOLE, NUMERALS, REAL;
definitions TARSKI, STRUCT_0, FUNCT_1, RELAT_2, WAYBEL_0, ORDINAL1, XBOOLE_0,
SQUARE_1, VALUED_0, ORDERS_2, GROUP_10;
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, RELAT_2, BAGORDER, WAYBEL_0, WAYBEL_4, XXREAL_0,
RELAT_1, ORDERS_1, FINSET_1, ORDINAL1, PUA2MSS1, GLIB_002, DICKSON,
FINSEQ_1, INT_5, RVSUM_1, UPROOTS, FINSEQ_2, CARD_3, FINSEQ_3, GRFUNC_1,
RAMSEY_1, REALSET1, SUBSET_1, PRE_POLY;
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
A: Y() = { F(w) where w is Element of A(): P[w] }
proof
B: A() is finite;
set Z = { F(w) where w is Element of A(): w in A() };
Z is finite from FRAENKEL:sch 21 (B);
then reconsider Z as finite set;
C: Z = { F(w) where w is Element of A(): w in A() };
D: card Z <= card A() from TREES_2:sch 3(C);
Y() c= Z proof
let x be set;
assume x in Y();
then ex w being Element of A() st x = F(w) & P[w] by A;
hence x in Z;
end;
then card Y() <= card Z by NAT_1:44;
hence card Y() <= card A() by D, XXREAL_0:2;
end;
theorem set00: :: 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 B: not x in X \ Y;
thus X \ (Y \/ {x}) = (X \ Y) \ {x} by XBOOLE_1:41
.= X \ Y by B, ZFMISC_1:65;
end;
registration
cluster empty -> c=-linear set;
coherence
proof let X be set such that
Z: X is empty;
let x be set;
thus thesis by Z;
end;
end;
registration let X be c=-linear set;
cluster -> c=-linear Subset of X;
coherence
proof
let Y be Subset of X;
let x, y be set;
assume x in Y & y in Y;
hence x,y are_c=-comparable by ORDINAL1:def 9;
end;
end;
theorem ssf0: :: 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;
A: F \/ G c= bool X \/ bool Y by XBOOLE_1:13;
bool X \/ bool Y c= bool (X \/ Y) by ZFMISC_1:81;
hence F \/ G is Subset-Family of X \/ Y by A, XBOOLE_1:1;
end;
theorem SPpart0: :: 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
A: X misses Y;
set PR = F \/ G; set XY = X \/ Y;
B: PR is Subset-Family of XY by ssf0;
C: union PR = union F \/ union G by ZFMISC_1:96
.= X \/ union G by EQREL_1:def 6 .= X \/ Y by EQREL_1:def 6;
now
let A be Subset of XY such that
A1: A in PR;
A in F or A in G by A1, XBOOLE_0:def 3;
hence A <> {} by EQREL_1:def 6;
let B be Subset of XY such that
B1: B in PR;
per cases by A1, B1, 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 6;
end;
suppose A in F & B in G or A in G & B in F;
hence A = B or A misses B by A, XBOOLE_1:64;
end;
end;
hence F \/ G is a_partition of X \/ Y by B, C, EQREL_1:def 6;
end;
theorem SPpart: :: 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 A: Y c< X;
then Ba: X \ Y <> {} by XBOOLE_1:105;
Y c= X by A, XBOOLE_0:def 8;
then C: Y \/ (X \ Y) = X by XBOOLE_1:45;
{ X \ Y } is a_partition of X \ Y by Ba, EQREL_1:48;
hence F \/ { X \ Y } is a_partition of X by XBOOLE_1:79, C, SPpart0;
end;
theorem Sinfset: :: 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 Function of NAT, X such that
A: 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:38;
ff is one-to-one by A, FUNCT_1:84;
then card ff = card rng ff by PRE_POLY:19;
then Z: card dom ff = card rng ff by CARD_1:104;
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:78;
hence card Y > n by Z, NAT_1:13;
end;
begin :: Cliques and stable sets
definition
let R be RelStr, S be Subset of R;
attr S is connected means :Lclique:
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 Subset of R;
coherence proof let S be Subset of R;
assume Z: S is trivial;
let x1, x2 be set;
thus thesis by Z, ZFMISC_1:def 10;
end;
end;
registration
let R be RelStr;
cluster clique Subset of R;
existence proof take {}R; let x1, x2 be set; thus thesis; end;
end;
definition
let R be RelStr;
mode Clique of R is clique Subset of R;
end;
theorem DClique: :: 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 A: RR is_connected_in S by Lclique;
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 A, RELAT_2:def 6;
hence a <= b or b <= a by ORDERS_2:def 9;
end;
assume
A: 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 set;
assume A1: x in S & y in S & x <> y;
then reconsider x' = x, y' = y as Element of R;
x' <= y' or y' <= x' by A1, A;
hence [x,y] in RR or [y,x] in RR by ORDERS_2:def 9;
end;
hence S is Clique of R by Lclique;
end;
registration
let R be RelStr;
cluster finite Clique of R;
existence proof take {}R; thus thesis; end;
end;
registration
let R be reflexive RelStr;
cluster connected -> strongly_connected 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 A: iR is_connected_in C by Lclique;
B: iR is_reflexive_in cR by ORDERS_2:def 4;
thus C is strongly_connected proof
let x, y be set such that
A1: x in C and
B1: 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 A1, B, RELAT_2:def 1;
end;
suppose x <> y;
hence [x,y] in the InternalRel of R or [y,x] in the InternalRel of R
by A1, B1, A, RELAT_2:def 6;
end;
end;
end;
end;
registration
let R be non empty RelStr;
cluster finite non empty 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 A: a1 <> a2;
A1: a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
assume {a1,a2} is Clique of R;
hence thesis by A1, A, DClique;
end;
theorem Clique36b: :: 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 A2: a1 <= a2 or a2 <= a1;
now
let x,y be Element of R;
assume x in {a1,a2} & y in {a1,a2};
then A4: (x = a1 or x = a2) & (y = a1 or y = a2) by TARSKI:def 2;
assume x <> y;
hence x <= y or y <= x by A2, A4;
end;
hence thesis by DClique;
end;
theorem Clique37: :: 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;
B1: iR is_connected_in C by Lclique;
iR is_connected_in S proof
let x1, x2 be set;
assume x1 in S & x2 in S & x1<>x2;
hence thesis by B1, RELAT_2:def 6;
end;
hence thesis by Lclique, 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 card B = n
proof
let R be RelStr, C be finite Clique of R, n be Nat such that
A: n <= card C;
consider BB being finite Subset of C such that
B: card BB = n by A, FINSEQ_4:87;
reconsider BB as finite Clique of R by Clique37;
take BB;
thus card BB = n by B;
end;
theorem ExtClique: :: 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
A: x is_maximal_in C and
B: x <= y;
C: x in C by A, WAYBEL_4:56;
B3a: the carrier of R is non empty by A, WAYBEL_4:56;
set Cb = C \/ {y};
D: Cb c= the carrier of R proof
let x be set;
assume A1: x in Cb;
per cases by A1, 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 B3a;
end;
end;
now
let a, b be Element of R such that
A3: a in Cb & b in Cb and
A3a: a <> b;
per cases by A3, XBOOLE_0:def 3;
suppose a in C & b in C;
hence a <= b or b <= a by A3a, DClique;
end;
suppose that
S1: a in C and
T1: b in {y};
A4: b = y by T1, TARSKI:def 1;
B4: not x < a by A, S1, WAYBEL_4:56;
per cases;
suppose x <> a;
then a <= x or x <= a by S1, C, DClique;
hence a <= b or b <= a by B, A4, ORDERS_2:26,B4,ORDERS_2:def 10;
end;
suppose x = a;
hence a <= b or b <= a by B, T1, TARSKI:def 1;
end;
end;
suppose that
S1: a in {y} and
T1: b in C;
A4: a = y by S1, TARSKI:def 1;
B4: not x < b by A, T1, WAYBEL_4:56;
per cases;
suppose x <> b;
then b <= x or x <= b by T1, C, DClique;
hence a <= b or b <= a by B, A4, ORDERS_2:26, B4,ORDERS_2:def 10;
end;
suppose x = b;
hence a <= b or b <= a by B, S1, 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 A3a;
end;
end;
hence C \/ {y} is Clique of R by D, DClique;
end;
theorem ExtCliquemin: :: 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
A: x is_minimal_in C and
B: y <= x;
C: x in C by A, WAYBEL_4:57;
B3a: the carrier of R is non empty by A, WAYBEL_4:57;
set Cb = C \/ {y};
D: Cb c= the carrier of R proof
let x be set;
assume A1: x in Cb;
per cases by A1, 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 B3a;
end;
end;
now
let a, b be Element of R such that
A3: a in Cb & b in Cb and
A3a: a <> b;
per cases by A3, XBOOLE_0:def 3;
suppose a in C & b in C;
hence a <= b or b <= a by A3a, DClique;
end;
suppose that
S1: a in C and
T1: b in {y};
A4: b = y by T1, TARSKI:def 1;
B4: not a < x by A, S1, WAYBEL_4:57;
per cases;
suppose S2: a <> x;
then not a <= x by B4, ORDERS_2:def 10;
then x <= a by S1, C, S2, DClique;
hence a <= b or b <= a by B, A4, ORDERS_2:26;
end;
suppose x = a;
hence a <= b or b <= a by B, T1, TARSKI:def 1;
end;
end;
suppose that
S1: a in {y} and
T1: b in C;
A4: a = y by S1, TARSKI:def 1;
B4: not b < x by A, T1, WAYBEL_4:57;
per cases;
suppose S2: b <> x;
then not b <= x by B4, ORDERS_2:def 10;
then x <= b by T1, C, S2, DClique;
hence a <= b or b <= a by B, A4, ORDERS_2:26;
end;
suppose x = b;
hence a <= b or b <= a by B, S1, 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 A3a;
end;
end;
hence C \/ {y} is Clique of R by D, DClique;
end;
definition
let R be RelStr, S be Subset of R;
attr S is stable means :LAChain:
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 Subset of R;
coherence
proof let S be Subset of R;
assume
Z: S is trivial;
let x, y being Element of R;
thus thesis by Z,ZFMISC_1:def 10;
end;
end;
registration
let R be RelStr;
cluster stable 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 StableSet of R;
existence proof
take {}R;
thus thesis;
end;
end;
registration
let R be non empty RelStr;
cluster finite non empty 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 A: a1 <> a2;
A1: a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
assume {a1,a2} is StableSet of R;
hence thesis by A1, A, LAChain;
end;
theorem AChain36b: :: 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
A2: not (a1 <= a2 or a2 <= a1);
set S = {a1,a2};
S is stable proof
let x, y be Element of R such that
B1: x in S & y in S & x <> y;
(x = a1 or x = a2) & (y = a1 or y = a2) by B1, TARSKI:def 2;
hence thesis by A2, B1;
end;
hence thesis;
end;
theorem ACClique: :: 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
A: a in A & b in A and
C: a in C & b in C;
assume S: a <> b;
reconsider a' = a, b' = b as Element of R by A;
not a' <= b' & not b' <= a' by A, S, LAChain;
hence contradiction by C, S, DClique;
end;
theorem AChain0: :: 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 proof
let x, y be Element of R such that
A: x in BB & y in BB & x <> y;
thus not x <= y & not y <= x by A, LAChain;
end;
hence thesis;
end;
theorem AChain1: :: 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
A: n <= card A;
consider BB being finite Subset of A such that
B: card BB = n by A, FINSEQ_4:87;
reconsider BB as finite StableSet of R by AChain0;
take BB;
thus card BB = n by B;
end;
begin :: Clique number and stability number
definition
let R be RelStr;
attr R is with_finite_clique# means :Lfheight:
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# RelStr;
coherence proof
let R be RelStr;
assume R is finite;
then reconsider R' = R as finite RelStr;
defpred P[Nat] means ex c being finite Clique of R st card c = $1;
P1: for k being Nat st P[k] holds k <= card R' by NAT_1:44;
card {}R = 0; then
P2: ex k being Nat st P[k];
consider k being Nat such that
B: P[k] and
C: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(P1,P2);
consider c being finite Clique of R such that
D: card c = k by B;
for D be finite Clique of R holds card(D) <= card(c) by D, C;
hence R is with_finite_clique# by Lfheight;
end;
end;
registration
let R be with_finite_clique# RelStr;
cluster -> finite Clique of R;
coherence proof
let D be Clique of R;
consider C being finite Clique of R such that
A: for D being finite Clique of R holds card(D) <= card(C) by Lfheight;
assume D is infinite;
then consider Y being finite Subset of D such that
B: card Y > card C by Sinfset;
Y is Clique of R by Clique37;
hence contradiction by B, A;
end;
end;
definition
let R be with_finite_clique# RelStr;
func clique# R -> Nat means :Lheight:
(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
A: for B being finite Clique of R holds card(B) <= card(A) by Lfheight;
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 A;
end;
uniqueness proof
let it1, it2 be Nat such that
A1a: ex S1 being finite Clique of R st card(S1) = it1 and
A1b: for T being finite Clique of R holds card(T) <= it1 and
A2a: ex S2 being finite Clique of R st card(S2) = it2 and
A2b: for T being finite Clique of R holds card(T) <= it2;
consider S1 being finite Clique of R such that
A1: card(S1) = it1 by A1a;
consider S2 being finite Clique of R such that
A2: card(S2) = it2 by A2a;
it1 <= it2 & it2 <= it1 by A1, A2, A1b, A2b;
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 Lheight;
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 Lheight;
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 A: [#]R is StableSet of R;
B: clique# R >= 0+1 by NAT_1:13;
consider A being finite Clique of R such that
C: card A = clique# R by Lheight;
assume clique# R <> 1;
then card A > 1 by B, C, XXREAL_0:1;
then consider a, b being set such that
D: a in A and
E: b in A and
F: a <> b by GLIB_002:1;
thus thesis by D, E, F, A, ACClique;
end;
theorem Height4: :: 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 A: clique# R = 1;
set cR = the carrier of R;
D: R is non empty by A;
now
let a, b be Element of R such that
a in cR and b in cR and
C1: a <> b;
assume a <= b or b <= a;
then D1: {a,b} is Clique of R by D, Clique36b;
card {a,b} = 2 by C1, CARD_2:76;
hence contradiction by D1, A, Lheight;
end;
hence [#]R is StableSet of R by LAChain;
end;
definition
let R be RelStr;
attr R is with_finite_stability# means :Lfwidth:
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# RelStr;
coherence proof
let R be RelStr;
assume R is finite;
then reconsider R' = R as finite RelStr;
defpred P[Nat] means
ex A being finite StableSet of R' st card A = $1;
P1: for k being Nat st P[k] holds k <= card R' by NAT_1:44;
{}R is StableSet of R & card {} = 0;
then P2: ex k being Nat st P[k];
consider k being Nat such that
A1: P[k] and
B1: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(P1, P2);
consider S being finite StableSet of R such that
C1: card S = k by A1;
take S;
let T be finite StableSet of R;
thus card T <= card S by C1, B1;
end;
end;
registration
let R be with_finite_stability# RelStr;
cluster -> finite StableSet of R;
coherence proof
consider A being finite StableSet of R such that
A: for B being finite StableSet of R holds card(A) >= card(B) by Lfwidth;
given B being StableSet of R such that
B: B is infinite;
consider C being finite Subset of B such that
C: card C > card A by B, Sinfset;
C is StableSet of R by AChain0;
hence contradiction by A, C;
end;
end;
definition
let R be with_finite_stability# RelStr;
func stability# R -> Nat means :Lwidth:
(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
A: for B being finite StableSet of R holds card(A) >= card(B) by Lfwidth;
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 A;
end;
uniqueness proof
let it1, it2 be Nat such that
Aa: ex S1 being finite StableSet of R st card S1 = it1 and
A1: for T being finite StableSet of R holds card(T) <= it1 and
Ab: ex S2 being finite StableSet of R st card S2 = it2 and
A2: for T being finite StableSet of R holds card(T) <= it2;
consider S1 being finite StableSet of R such that
A3: card S1 = it1 by Aa;
consider S2 being finite StableSet of R such that
A4: card S2 = it2 by Ab;
it1 <= it2 & it2 <= it1 by A1, A2, A3, A4;
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 Lwidth;
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 Lwidth;
hence thesis;
end;
end;
theorem Width3: :: 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 A: [#]R is Clique of R;
B: stability# R >= 0+1 by NAT_1:13;
consider A being finite StableSet of R such that
C: card(A) = stability# R by Lwidth;
assume stability# R <> 1;
then card A > 1 by B, C, XXREAL_0:1;
then consider a, b being set such that
D: a in A and
E: b in A and
F: a <> b by GLIB_002:1;
thus thesis by D, E, F, A, ACClique;
end;
theorem Width4: :: 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 A: stability# R = 1;
set cR = the carrier of R;
now
let a, b be Element of R such that
A1: a in cR and b in cR and
C1: a <> b;
E1: R is non empty by A1;
assume not (a <= b or b <= a);
then D1: {a,b} is StableSet of R by E1, AChain36b;
card {a,b} = 2 by C1, CARD_2:76;
hence contradiction by A, Lwidth, D1;
end;
hence [#]R is Clique of R by DClique;
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 RelStr;
coherence proof
let R be RelStr;
assume A: R is with_finite_clique#;
assume B: R is with_finite_stability#;
assume C: R is infinite;
reconsider R as with_finite_clique# with_finite_stability# RelStr by A, B;
consider C being finite Clique of R such that
D: card C = clique# R by Lheight;
consider An being finite StableSet of R such that
E: card(An) = stability# R by Lwidth;
set h = clique# R, w = stability# R;
hh: 0+1 <= h by C, NAT_1:13;
ww: 0+1 <= w by C, NAT_1:13;
set cR = the carrier of R, iR = the InternalRel of R;
cR: cR = [#]R;
per cases by hh, ww, XXREAL_0:1;
suppose h = 1;
then A1: cR is StableSet of R by cR, Height4;
consider Y being finite Subset of cR such that
B1: card Y > w by C, Sinfset;
Y is StableSet of R by A1, AChain0;
hence thesis by B1, Lwidth;
end;
suppose w = 1;
then A1: cR is Clique of R by cR, Width4;
consider Y being finite Subset of cR such that
B1: card Y > h by C, Sinfset;
Y is Clique of R by A1, Clique37;
hence thesis by B1, Lheight;
end;
suppose S1: h > 1 & w > 1;
set m = max(clique# R, stability# R) +1;
reconsider m as natural number;
consider r being natural number such that
G: 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
HY: card Y > r by C, Sinfset;
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
H1a: card Y <= card X by NAT_1:44, 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 };
As: A c= E proof
let x be set;
assume x in A;
then consider xx, yy being Element of R such that
D1: {xx,yy} = x and
E1: xx<>yy and
F1: xx in X and
G1: yy in X and xx <= yy or yy <= xx;
x is Subset of X & card x = 2
by D1, E1, F1, G1, ZFMISC_1:38, CARD_2:76;
hence thesis;
end;
Bs: B c= E proof
let x be set;
assume A3: x in B;
consider xx, yy being Element of R such that
D1: {xx,yy} = x and
E1: xx<>yy and
F1: xx in X and
G1: yy in X and not (xx <= yy or yy <= xx) by A3;
x is Subset of X & card x = 2
by D1, E1, F1, G1, ZFMISC_1:38, CARD_2:76;
hence thesis;
end;
AB: A in P & B in P by TARSKI:def 2;
Ha: now
assume A2: A = B;
consider a, b being set such that
B2: a in An and
C2: b in An and
D2: a <> b by S1, E, GLIB_002:1;
reconsider a, b as Element of R by B2, C2;
E2: not (a <= b or b <= a) by B2, C2, D2, LAChain;
a in Y \/ An & b in Y \/ An by B2, C2, XBOOLE_0:def 3;
then a in X & b in X by XBOOLE_0:def 3;
then {a,b} in B by E2, D2;
then consider aa, bb being Element of R such that
F2: {a,b} = {aa, bb} and
aa <> bb & aa in X & bb in X and
H2: aa <= bb or bb <= aa by A2;
a = aa & b = bb or a = bb & b = aa by F2, ZFMISC_1:10;
hence contradiction by H2, B2, C2, D2, LAChain;
end;
Hca: P c= bool E proof
let x be set;
assume x in P;
then x c= E by As, Bs, TARSKI:def 2;
hence thesis;
end;
Hb: union P = E proof
thus union P c= E proof
let x be set;
assume x in union P;
then consider Y being set such that
A3: x in Y and
B3: Y in P by TARSKI:def 4;
Y = A or Y = B by B3, TARSKI:def 2;
hence thesis by A3, As, Bs;
end;
thus E c= union P proof
let x be set;
assume x in E;
then consider xx being Subset of X such that
A2: x = xx and
B2: card xx = 2;
consider a, b being set such that
C2: a <> b and
D2: xx = {a,b} by B2, CARD_2:79;
a in xx & b in xx by D2, TARSKI:def 2;
then a in X & b in X;
then reconsider a, b as Element of R;
E2a: a in xx & b in xx by D2, 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 E2a, C2;
hence x in union P by A2, D2, AB, 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
A2: a in P;
thus a<>{} proof
per cases by A2, TARSKI:def 2;
suppose S2: a = A;
consider aa, bb being set such that
B3: aa in C and
C3: bb in C and
D3: aa <> bb by S1, D, GLIB_002:1;
reconsider aa, bb as Element of R by B3, C3;
E3: aa <= bb or bb <= aa by B3, C3, D3, DClique;
aa in Y \/ An \/ C & bb in Y \/ An \/ C by B3, C3, XBOOLE_0:def 3;
then {aa,bb} in A by E3, D3;
hence thesis by S2;
end;
suppose S2: a = B;
consider aa, bb being set such that
B3: aa in An and
C3: bb in An and
D3: aa <> bb by S1, E, GLIB_002:1;
reconsider aa, bb as Element of R by B3, C3;
E3: not (aa <= bb or bb <= aa) by B3, C3, D3, LAChain;
aa in Y \/ An & bb in Y \/ An by B3, C3, XBOOLE_0:def 3;
then aa in X & bb in X by XBOOLE_0:def 3;
then {aa,bb} in B by E3, D3;
hence thesis by S2;
end;
end;
let b be Subset of E such that
B2: b in P;
assume C2: a <> b;
assume D2: a meets b;
(a = A or a = B) & (b = A or b = B) by A2,B2, TARSKI:def 2;
then A /\ B <> {} by C2, D2, XBOOLE_0:def 7;
then consider x being set such that
E2: x in A /\ B by XBOOLE_0:def 1;
x in A by E2, XBOOLE_0:def 4;
then consider xx, yy being Element of R such that
F1: {xx,yy} = x and xx<>yy & xx in X & yy in X and
G1: xx <= yy or yy <= xx;
x in B by E2, XBOOLE_0:def 4;
then consider x2, y2 being Element of R such that
H1: {x2,y2} = x and x2<>y2 & x2 in X & y2 in X and
I1: not (x2 <= y2 or y2 <= x2);
xx = x2 & yy = y2 or xx = y2 & yy = x2 by F1, H1, ZFMISC_1:10;
hence contradiction by G1, I1;
end;
then reconsider P as a_partition of E by Hb, Hca, EQREL_1:def 6;
J: card P = 2 by Ha, CARD_2:76;
consider S being Subset of X such that
K: card S >= m and
L: S is_homogeneous_for P by H1a, J, G, HY, 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
mh: card S > clique# R by K, XXREAL_0:2;
max(clique# R, stability# R) >= stability# R by XXREAL_0:25;
then m > stability# R by NAT_1:13;
then
mw: card S > stability# R by K, XXREAL_0:2;
consider p being Element of P such that
M: the_subsets_of_card(2,S) c= p by L, RAMSEY_1:def 1;
per cases by TARSKI:def 2;
suppose S1: p = A;
now
let x, y be Element of R such that
A1: x in S and
B1: y in S and
C1: x <> y;
{x,y} is Subset of S & card {x,y} = 2
by A1, B1, C1, ZFMISC_1:38, CARD_2:76;
then {x,y} in the_subsets_of_card(2,S);
then {x,y} in A by S1, M;
then consider xx, yy being Element of R such that
D1: {xx,yy} = {x,y} and xx<>yy & xx in X & yy in X and
E1: xx <= yy or yy <= xx;
xx = x & yy = y or xx = y & yy = x by D1, ZFMISC_1:10;
hence x <= y or y <= x by E1;
end;
then S is Clique of R by DClique;
hence contradiction by mh, Lheight;
end;
suppose S1: p = B;
S is stable proof
let x, y being Element of R such that
A1: x in S and
B1: y in S and
C1: x <> y;
{x,y} is Subset of S & card {x,y} = 2
by A1, B1, C1, ZFMISC_1:38, CARD_2:76;
then {x,y} in the_subsets_of_card(2,S);
then {x,y} in B by S1, M;
then consider xx, yy being Element of R such that
D1: {xx,yy} = {x,y} and xx<>yy & xx in X & yy in X and
E1: not (xx <= yy or yy <= xx);
xx = x & yy = y or xx = y & yy = x by D1, ZFMISC_1:10;
hence not x <= y & not y <= x by E1;
end;
hence contradiction by mw, Lwidth;
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 ABAC0: :: 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
A: z in Upper A and
B: z in Lower A;
per cases;
suppose z in A;
hence thesis;
end;
suppose S1: not z in A;
A1: z in uparrow A by A, S1, XBOOLE_0:def 3;
B1: z in downarrow A by B, S1, XBOOLE_0:def 3;
reconsider y = z as Element of R by A;
consider x being Element of R such that
E: x <= y and
F: x in A by A1, WAYBEL_0:def 16;
reconsider x' = z as Element of R by B;
consider y' being Element of R such that
I: x' <= y' and
J: y' in A by B1,WAYBEL_0:def 15;
x <= y' by E, I, YELLOW_0:def 2;
then x = y' by F, J, LAChain;
hence z in A by E, F, I, YELLOW_0:def 3;
end;
end;
theorem ABunion: :: 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
AA: card A = stability# R;
set cP = the carrier of R;
cP c= Upper A \/ Lower A proof
let x be set;
assume A: x in cP;
assume B: not x in Upper A \/ Lower A;
reconsider x as Element of cP by A;
C: not x in Upper A by B, XBOOLE_0:def 3;
Ca: not x in A by C, XBOOLE_0:def 3;
Cb: not x in uparrow A by C, XBOOLE_0:def 3;
D: not x in Lower A by B, XBOOLE_0:def 3;
Db: not x in downarrow A by D, XBOOLE_0:def 3;
set Ax = A \/ {x};
Ka: {x} c= the carrier of R by A, ZFMISC_1:37;
now
let a, b be Element of R such that
A1: a in Ax and
B1: b in Ax and
C1: a <> b;
per cases by A1, B1, XBOOLE_0:def 3;
suppose a in A & b in A;
hence not a <= b & not b <= a by C1, LAChain;
end;
suppose S1: a in A & b in {x};
then b = x by TARSKI:def 1;
hence not a <= b & not b <= a by Cb,WAYBEL_0:def 16,Db,WAYBEL_0:def 15,S1;
end;
suppose S1: a in {x} & b in A;
then a = x by TARSKI:def 1;
hence not a <= b & not b <= a by Cb,WAYBEL_0:def 16,Db,WAYBEL_0:def 15,S1;
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 C1;
end;
end;
then P: Ax is StableSet of R by Ka, XBOOLE_1:8, LAChain;
card Ax = card A + 1 by Ca, CARD_2:54;
then card Ax > card A by NAT_1:13;
hence contradiction by Lwidth, AA, P;
end;
hence Upper A \/ Lower A = [#]R by XBOOLE_0:def 10;
end;
theorem Pminmin: :: 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
A: x is_minimal_in Lower S;
set cR = the carrier of R;
B: x in Lower S by A, WAYBEL_4:57;
assume not x is_minimal_in [#]R;
then consider y being Element of R such that y in cR and
E: y < x by B, WAYBEL_4:57;
per cases by B, XBOOLE_0:def 3;
suppose S1: x in S;
y <= x by E, ORDERS_2:def 10;
then y in downarrow S by S1, WAYBEL_0:def 15;
then y in Lower S by XBOOLE_0:def 3;
hence thesis by A, E, WAYBEL_4:57;
end;
suppose S1: x in downarrow S;
consider x'' being Element of R such that
H: x <= x'' and
I: x'' in S by S1, WAYBEL_0:def 15;
y <= x by E, ORDERS_2:def 10; then
J: y <= x'' by H, YELLOW_0:def 2;
y in downarrow S by I, J, WAYBEL_0:def 15;
then y in Lower S by XBOOLE_0:def 3;
hence contradiction by A, E, WAYBEL_4:57;
end;
end;
theorem Pmaxmax: :: 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
A: x is_maximal_in Upper S;
set cR = the carrier of R;
B: x in Upper S by A, WAYBEL_4:56;
assume not x is_maximal_in [#]R;
then consider y being Element of R such that y in cR and
E: x < y by B, WAYBEL_4:56;
per cases by B, XBOOLE_0:def 3;
suppose S1: x in S;
x <= y by E, ORDERS_2:def 10;
then y in uparrow S by S1, WAYBEL_0:def 16;
then y in Upper S by XBOOLE_0:def 3;
hence thesis by A, E, WAYBEL_4:56;
end;
suppose x in uparrow S;
then consider x'' being Element of R such that
H: x'' <= x and
I: x'' in S by WAYBEL_0:def 16;
x <= y by E, ORDERS_2:def 10;
then x'' <= y by H, YELLOW_0:def 2;
then y in uparrow S by I, WAYBEL_0:def 16;
then y in Upper S by XBOOLE_0:def 3;
hence contradiction by A, E, WAYBEL_4:56;
end;
end;
definition
let R be RelStr;
set cR = the carrier of R;
func minimals R -> Subset of R means :Lmin:
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[set] means ex a being Element of R st a = $1 & a is_minimal_in cR;
consider X being set such that
A: for x being set holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1;
B: now
assume S1: cR is non empty;
for x being set st x in X holds x in cR by A;
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 A;
hence x in X iff x is_minimal_in cR by A, S1;
end;
now
reconsider X = {} as Subset of R by XBOOLE_1:2;
take X;
thus X = {};
end;
hence thesis by B;
end;
uniqueness proof
let it1, it2 be Subset of R;
now assume that R is non empty and
A1: for x being Element of R holds x in it1 iff x is_minimal_in cR and
A2: for x being Element of R holds x in it2 iff x is_minimal_in cR;
now
let x be set;
now
assume A3: x in it1 or x in it2;
then reconsider x' = x as Element of R;
x' is_minimal_in cR by A3, A1, A2;
hence x in it1 & x in it2 by A1, A2;
end;
hence x in it1 iff x in it2;
end;
hence it1 = it2 by TARSKI:2;
end;
hence thesis;
end;
func maximals R -> Subset of R means :Lmax:
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[set] means ex a being Element of R st a = $1 & a is_maximal_in cR;
consider X being set such that
A: for x being set holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1;
B: now
assume S1: cR is non empty;
for x being set st x in X holds x in cR by A;
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 A;
hence x in X iff x is_maximal_in cR by A, S1;
end;
now
reconsider X = {} as Subset of R by XBOOLE_1:2;
take X;
thus X = {};
end;
hence thesis by B;
end;
uniqueness proof
let it1, it2 be Subset of R;
now assume that R is non empty and
A1: for x being Element of R holds x in it1 iff x is_maximal_in cR and
A2: for x being Element of R holds x in it2 iff x is_maximal_in cR;
now
let x be set;
now
assume A3: x in it1 or x in it2;
then reconsider x' = x as Element of R;
x' is_maximal_in cR by A3, A1, A2;
hence x in it1 & x in it2 by A1, A2;
end;
hence x in it1 iff x in it2;
end;
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
AA: for D being finite Clique of R holds card(D) <= card(CL) by Lfheight;
card {the Element of R} <= card CL by AA;
then CL <> {};
then consider y being Element of R such that y in CL and
D: y is_maximal_wrt CL, iP by BAGORDER:7;
E: y is_maximal_in CL by D, WAYBEL_4:def 25;
F: cP = [#]R;
now
assume not y is_maximal_in cP;
then consider z being Element of R such that z in cP and
C1: y < z by WAYBEL_4:56;
D1: y <= z by C1, ORDERS_2:def 10;
set C = CL \/ {z};
reconsider C as finite Clique of R by D1, E, ExtClique;
not z in CL by E, C1, WAYBEL_4:56;
then card C = card CL + 1 by CARD_2:54;
then card CL + 1 <= card CL + 0 by AA;
hence contradiction by XREAL_1:8;
end;
hence thesis by F, Lmax;
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
AA: for D being finite Clique of R holds card(D) <= card(CL) by Lfheight;
card {the Element of R} <= card CL by AA;
then CL <> {};
then consider y being Element of R such that y in CL and
D: y is_minimal_wrt CL, iP by BAGORDER:8;
E: y is_minimal_in CL by D, WAYBEL_4:def 27;
F: cP = [#]R;
now
assume not y is_minimal_in cP;
then consider z being Element of R such that z in cP and
C1: z < y by WAYBEL_4:57;
D1: z <= y by C1, ORDERS_2:def 10;
set C = CL \/ {z};
reconsider C as finite Clique of R by D1, E, ExtCliquemin;
not z in CL by E, C1, WAYBEL_4:57;
then card C = card CL + 1 by CARD_2:54;
then card CL + 1 <= card CL + 0 by AA;
hence contradiction by XREAL_1:8;
end;
hence thesis by F, Lmin;
end;
end;
registration let R be RelStr;
cluster minimals R -> stable;
coherence
proof
set mR = minimals R, cR = the carrier of R;
let x, y be Element of R such that
A: x in mR and
B: y in mR and
C: x <> y;
D: R is non empty by A;
y is_minimal_in [#]R by B, D, Lmin;
then not y > x by A, WAYBEL_4:57;
hence not x <= y by C, ORDERS_2:def 10;
x is_minimal_in [#]R by A, D, Lmin;
then not x > y by B, WAYBEL_4:57;
hence not y <= x by C, ORDERS_2:def 10;
end;
cluster maximals R -> stable;
coherence
proof
set mR = maximals R, cR = the carrier of R;
let x, y be Element of R such that
A: x in mR and
B: y in mR and
C: x <> y;
D: R is non empty by A;
x is_maximal_in [#]R by A, D, Lmax;
then not y > x by B, WAYBEL_4:56;
hence not x <= y by C, ORDERS_2:def 10;
y is_maximal_in [#]R by B, D, Lmax;
then not x > y by A, WAYBEL_4:56;
hence not y <= x by C, ORDERS_2:def 10;
end;
end;
theorem PCAamin: :: 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 set such that
B: x in minimals R and
C: not x in A by TARSKI:def 3;
assume D: minimals R c= Upper A;
reconsider x' = x as Element of R by B;
R is non empty by B;
then B1: x' is_minimal_in [#]R by B, Lmin;
x' in uparrow A by C, B, D, XBOOLE_0:def 3;
then consider x'' being Element of R such that
C1: x'' <= x' and
D1: x'' in A by WAYBEL_0:def 16;
now assume x'' <> x';
then x'' < x' by C1, ORDERS_2:def 10;
hence contradiction by B, B1, WAYBEL_4:57;
end;
hence contradiction by D1, C;
end;
theorem PCAbmax: :: 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
A: not maximals R c= A;
consider x being set such that
B: x in maximals R and
C: not x in A by A, TARSKI:def 3;
assume D: maximals R c= Lower A;
reconsider x' = x as Element of R by B;
R is non empty by B;
then B1: x' is_maximal_in [#]R by B, Lmax;
x' in downarrow A by C, B, D, XBOOLE_0:def 3;
then consider x'' being Element of R such that
C1: x' <= x'' and
D1: x'' in A by WAYBEL_0:def 15;
now assume x'' <> x';
then x' < x'' by C1, ORDERS_2:def 10;
hence contradiction by B, B1, WAYBEL_4:56;
end;
hence contradiction by D1, C;
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 SPClique: :: 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;
Aa: the carrier of subrelstr S = S by YELLOW_0:def 15;
now
let a, b be Element of R such that
A1: a in C and
B1: b in C and
C1: a <> b;
reconsider a' = a, b' = b as Element of subrelstr S by A1,B1;
a' <= b' or b' <= a' by A1, B1, C1, DClique;
hence a <= b or b <= a by YELLOW_0:60;
end;
hence C is Clique of R by Aa, XBOOLE_1:1, DClique;
end;
theorem SPClique1: :: 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;
Aa: CS c= S by XBOOLE_1:17;
B: S = the carrier of sS by YELLOW_0:def 15;
now
let a, b be Element of sS;
assume Z0: a in CS;
assume Z1: b in CS;
assume Z2a: a <> b;
ZZ: a in S & b in S by Z0, Z1, XBOOLE_0:def 4;
Z2: S is non empty by Z0;
Z4: R is non empty by Z0;
reconsider a' = a, b' = b as Element of R by Z2, Z4, YELLOW_0:59;
a' in C & b' in C by Z0, Z1, XBOOLE_0:def 4;
then a' <= b' or b' <= a' by Z2a, DClique;
hence a <= b or b <= a by ZZ, B, YELLOW_0:61;
end;
hence C /\ S is Clique of subrelstr S by DClique, Aa, YELLOW_0:def 15;
end;
theorem SPAChain1: :: 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 S1: 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 S2: 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
A1: x in A and
B1: y in A and
C1: x <> y;
reconsider x' = x, y' = y as Element of sS by A1, B1;
not x' <= y' & not y' <= x' by A1, B1, C1, LAChain;
hence not x <= y & not y <= x by S1, S2, YELLOW_0:61;
end;
hence thesis;
end;
end;
end;
theorem SPAChain: :: 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 S1: R is non empty;
per cases;
suppose S is empty;
then A /\ S = {}sS;
hence A /\ S is StableSet of sS;
end;
suppose S2: 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
A1: x in AS and
B1: y in AS and
C1: x <> y;
reconsider x' = x, y' = y as Element of R by S1, S2, YELLOW_0:59;
D1: x' in A by A1, XBOOLE_0:def 4;
E1: y' in A by B1, XBOOLE_0:def 4;
not x' <= y' & not y' <= x' by D1, E1, C1, LAChain;
hence not x <= y & not y <= x by YELLOW_0:60;
end;
hence A /\ S is StableSet of sS;
end;
end;
end;
theorem SPmax: :: 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
A: x = y and
B: x is_maximal_in B;
C: x in B by B, WAYBEL_4:56;
assume not y is_maximal_in B;
then consider z being Element of R such that
A1: z in B and
B1: y < z by A, C, WAYBEL_4:56;
C1: y <= z by B1, ORDERS_2:def 10;
reconsider z' = z as Element of subrelstr S by A1;
x <= z' by A1, C1, A, YELLOW_0:61;
then x < z' by B1, A, ORDERS_2:def 10;
hence contradiction by A1, B, WAYBEL_4:56;
end;
theorem SPmin: :: 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
A: x = y and
B: x is_minimal_in B;
C: x in B by B, WAYBEL_4:57;
assume not y is_minimal_in B;
then consider z being Element of R such that
A1: z in B and
B1: z < y by A, C, WAYBEL_4:57;
C1: z <= y by B1, ORDERS_2:def 10;
reconsider z' = z as Element of subrelstr S by A1;
z' <= x by A1, C1, A, YELLOW_0:61;
then z' < x by B1, A, ORDERS_2:def 10;
hence contradiction by A1, B, WAYBEL_4:57;
end;
theorem PbeSmax: :: 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
A: a in A and
B: a in C and
C: b in C;
set ap = subrelstr Lower A;
reconsider a' = a as Element of ap by B;
Da: b in the carrier of ap by C;
reconsider b' = b as Element of ap by C;
D: b' in Lower A by Da, YELLOW_0:def 15;
E: C is Clique of R by SPClique;
per cases by D, XBOOLE_0:def 3;
suppose b' in A;
hence thesis by A,B,C,E,ACClique;
end;
suppose b' in downarrow A;
then consider c being Element of R such that
A1: b <= c and
B1: c in A by WAYBEL_0:def 15;
per cases;
suppose Ax: a <> b;
per cases by Ax, B, C, DClique;
suppose a' <= b';
then S1a: a <= b by YELLOW_0:60;
a <= c by S1a, A1, YELLOW_0:def 2;
hence thesis by B1, A1, A, LAChain;
end;
suppose b' <= a';
hence thesis by YELLOW_0:60;
end;
end;
suppose a = b;
hence thesis;
end;
end;
end;
theorem PabSmin: :: 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
A: a in A and
B: a in C and
C: b in C;
set ap = subrelstr Upper A;
reconsider a' = a as Element of ap by B;
Da: b in the carrier of ap by C;
reconsider b' = b as Element of ap by C;
D: b' in Upper A by Da, YELLOW_0:def 15;
E: C is Clique of R by SPClique;
per cases by D, XBOOLE_0:def 3;
suppose b' in A;
hence thesis by A, B, C, E, ACClique;
end;
suppose b' in uparrow A;
then consider c being Element of R such that
A1: c <= b and
B1: c in A by WAYBEL_0:def 16;
per cases;
suppose Ax: a <> b;
per cases by Ax, B, C, DClique;
suppose a' <= b';
hence thesis by YELLOW_0:60;
end;
suppose b' <= a';
then S1a: b <= a by YELLOW_0:60;
c <= a by S1a, A1, YELLOW_0:def 2;
hence thesis by B1, A1, A, LAChain;
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
A: for D being finite Clique of R holds card(D) <= card(C) by Lfheight;
set sS = subrelstr S;
defpred P[Nat] means ex c being finite Clique of sS st card c = $1;
P1: 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
A1: card c = k;
c is finite Clique of R by SPClique;
hence thesis by A1, A;
end;
card {}sS = 0; then
P2: ex k being Nat st P[k];
consider k being Nat such that
B: P[k] and
C: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(P1,P2);
consider c being finite Clique of sS such that
D: card c = k by B;
for D being finite Clique of sS holds card(D) <= card(c) by D, C;
hence sS is with_finite_clique# by Lfheight;
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
A: for B being finite StableSet of R holds card(A) >= card(B) by Lfwidth;
assume Aa: 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);
P1: P[0] proof
reconsider C = {}(subrelstr S) as finite StableSet of subrelstr S;
take C;
thus card C = 0;
hence thesis by Aa, Lfwidth;
end;
P2: 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
C1: ex B being finite StableSet of subrelstr S st n < card(B);
consider B being finite Subset of subrelstr S such that
D1: n < card(B) & B is StableSet of subrelstr S by C1;
n+1 <= card B by D1, NAT_1:13;
then consider BB being finite StableSet of subrelstr S such that
E1: card BB = n+1 by D1, AChain1;
take BB;
thus card BB = n+1 by E1;
consider Bb being finite StableSet of subrelstr S such that
D1b: card BB < card(Bb) by Aa, Lfwidth;
take Bb;
thus n+1 < card Bb by D1b, E1;
end;
Q: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
consider C being finite StableSet of subrelstr S such that
card C = card A and
S: ex B being finite StableSet of subrelstr S st card A < card(B) by Q;
consider B being finite StableSet of subrelstr S such that
T: card A < card(B) by S;
B is StableSet of R by SPAChain1;
hence contradiction by A, T;
end;
end;
theorem Pmaxmin: :: 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 cR = the carrier of R, iR = the InternalRel of R;
set sx = Lower {x}; set sL = subrelstr sx;
reconsider sL as with_finite_clique# non empty antisymmetric transitive RelStr;
consider y being set such that
A: y in minimals sL by XBOOLE_0:def 1;
reconsider y as Element of sL by A;
C: [#]sL = sx by YELLOW_0:def 15;
B: y is_minimal_in sx by A, C, Lmin;
reconsider y' = y as Element of R by YELLOW_0:59;
take y';
sx c= the carrier of sL by YELLOW_0:def 15;
hence y' is_minimal_in [#]R by B, SPmin, Pminmin;
per cases;
suppose y' = x;
hence thesis;
end;
suppose y' <> x;
then not y' in {x} by TARSKI:def 1;
then y' in downarrow x by XBOOLE_0:def 3, C;
then y' <= x by WAYBEL_0:17;
hence thesis by ORDERS_2:def 10;
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 set;
assume A1: x in cR;
then reconsider x' = x as Element of R;
B1: R is non empty by A1;
consider y being Element of R such that
C1: y is_minimal_in [#]R and
D1: y = x' or y < x' by B1, Pmaxmin;
E1: y in minimals R by C1, B1, Lmin;
per cases by D1;
suppose x' = y;
hence thesis by E1, XBOOLE_0:def 3;
end;
suppose y < x';
then y <= x' by ORDERS_2:def 10;
then x in uparrow minimals R by E1, WAYBEL_0:def 16;
hence x in ap by XBOOLE_0:def 3;
end;
end;
hence thesis by XBOOLE_0:def 10;
end;
theorem Pminmax: :: 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 cR = the carrier of R;
set ax = Upper {x}; set sU = subrelstr ax;
reconsider sU as with_finite_clique# non empty antisymmetric transitive RelStr;
consider y being set such that
A: y in maximals sU by XBOOLE_0:def 1;
reconsider y as Element of sU by A;
C: [#]sU = ax by YELLOW_0:def 15;
B: y is_maximal_in ax by A, C, Lmax;
reconsider y' = y as Element of R by YELLOW_0:59;
take y';
ax c= the carrier of sU by YELLOW_0:def 15;
hence y' is_maximal_in [#]R by B, SPmax, Pmaxmax;
per cases;
suppose y' = x;
hence thesis;
end;
suppose y' <> x;
then not y' in {x} by TARSKI:def 1;
then y' in uparrow x by XBOOLE_0:def 3, C;
then x <= y' by WAYBEL_0:18;
hence thesis by ORDERS_2:def 10;
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 set;
assume A1: x in cP;
then reconsider x' = x as Element of P;
B1: P is non empty by A1;
consider y being Element of P such that
C1: y is_maximal_in [#]P and
D1: y = x' or y > x' by B1, Pminmax;
E1: y in maximals P by C1, B1, Lmax;
per cases by D1;
suppose x' = y;
hence thesis by E1, XBOOLE_0:def 3;
end;
suppose y > x';
then x' <= y by ORDERS_2:def 10;
then x in downarrow maximals P by E1, WAYBEL_0:def 15;
hence x in ap by XBOOLE_0:def 3;
end;
end;
hence thesis by XBOOLE_0:def 10;
end;
theorem PCAmin: :: 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
A: minimals R c= A;
A c= minimals R proof
let x be set;
assume A1: x in A;
then A1a: R is non empty;
reconsider x' = x as Element of R by A1;
consider y being Element of R such that
B1: y is_minimal_in [#]R and
C1: y = x' or y < x' by A1a, Pmaxmin;
D1: y = x' or y <= x' by C1, ORDERS_2:def 10;
y in minimals R by A1a, B1, Lmin;
hence x in minimals R by A, A1, D1, LAChain;
end;
hence A = minimals R by A, XBOOLE_0:def 10;
end;
theorem PCAmax: :: 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
A: maximals R c= A;
A c= maximals R proof
let x be set;
assume A1: x in A;
then A1a: R is non empty;
reconsider x' = x as Element of R by A1;
consider y being Element of R such that
B1: y is_maximal_in [#]R and
C1: y = x' or x' < y by A1a, Pminmax;
D1: y = x' or x' <= y by C1, ORDERS_2:def 10;
y in maximals R by A1a, B1, Lmax;
hence x in maximals R by A, A1, D1, LAChain;
end;
hence A = maximals R by A, XBOOLE_0:def 10;
end;
theorem Hsubp0: :: 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
a: card c = clique# s by Lheight;
c is Clique of R by SPClique;
hence clique# subrelstr S <= clique# R by Lheight, a;
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
A: card C = clique# R and
B: C c= S;
C = C /\ S by B, XBOOLE_1:28; then
C: C is Clique of subrelstr S by SPClique1;
consider Cs being Clique of subrelstr S such that
As: card(Cs) = clique# subrelstr S by Lheight;
D: card C <= card Cs by C, As, Lheight;
clique# subrelstr S <= clique# R by Hsubp0;
hence clique# subrelstr S = clique# R by As, A, D, XXREAL_0:1;
end;
theorem Wsubp0: :: 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
As: card(As) = stability# subrelstr S by Lwidth;
As is StableSet of R by SPAChain1;
hence stability# subrelstr S <= stability# R by As, Lwidth;
end;
theorem Wsubp1: :: 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
A: card A = stability# R and
B: A c= S;
A = A /\ S by B, XBOOLE_1:28; then
C: A is StableSet of subrelstr S by SPAChain;
consider As being StableSet of subrelstr S such that
As: card(As) = stability# subrelstr S by Lwidth;
D: card A <= card As by C, As, Lwidth;
stability# subrelstr S <= stability# R by Wsubp0;
hence stability# subrelstr S = stability# R by As, A, D, 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 :LCpart:
for x being set st x in P holds x is Clique of R;
end;
registration let R be RelStr;
cluster Clique-wise 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:54;
take S ;
thus for x being set st x in S holds x is Clique of R;
end;
suppose S: R is non empty;
take S = SmallestPartition cR;
let z being set;
assume A: z in S;
S = {{x} where x is Element of cR: not contradiction} by S, EQREL_1:46;
then consider x being Element of cR such that
B: z = {x} and not contradiction by A;
thus z is Clique of R by B, S, SUBSET_1:55;
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 a_partition of the carrier of R;
coherence
proof let P be a_partition of the carrier of R such that P is empty;
let x be set;
thus thesis;
end;
end;
theorem Chpw: :: 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 A: card(C) < stability# R;
consider A being StableSet of R such that
B: card A = stability# R by Lwidth;
card card C = card C & card card A = card A;
then C: card C in card A by A, B, NAT_1:42;
set cR = the carrier of R;
per cases;
suppose R is empty;
hence contradiction by A;
end;
suppose S1: R is non empty;
defpred P[set,set] means
$1 in A & $2 in C & $1 in $2;
P: for x being set st x in A ex y being set st y in C & P[x,y] proof
let x be set such that
A1: x in A;
reconsider x' = x as Element of R by A1;
cR is non empty by S1;
then x' in cR;
then x in union C by EQREL_1:def 6;
then consider y being set such that
B1: x in y and
C1: y in C by TARSKI:def 4;
take y;
thus thesis by A1, B1, C1;
end;
consider f being Function of A, C such that
Q: for x being set st x in A holds P[x,f.x] from FUNCT_2:sch 1(P);
consider x,y being set such that
A1: x in A and
B1: y in A and
C1: x <> y and
D1: f.x = f.y by S1, C, FINSEQ_4:80;
f.x in C by A1, FUNCT_2:7; then
E1: f.x is Clique of R by LCpart;
x in f.x & y in f.x by D1, A1, B1, Q;
hence contradiction by E1, A1, B1, C1, ACClique;
end;
end;
theorem ACpart1: :: 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
A: card C = card A;
set cR = the carrier of R;
per cases;
suppose S1: R is empty;
AA: the carrier of R is empty by S1;
A1: C = {} by AA, EQREL_1:41;
consider f being Function of A, C;
dom f = {} by S1;
then reconsider f = {} as Function of A, C by RELAT_1:64;
G1: f is onto by RELAT_1:60, A1, FUNCT_2:def 3;
take f;
thus f is bijective by G1;
thus thesis;
end;
suppose S1: R is non empty;
defpred P[set,set] means
$1 in A & $2 in C & $1 in $2;
P: for x being set st x in A ex y being set st y in C & P[x,y] proof
let x be set;
assume A1: x in A;
then reconsider x' = x as Element of R;
cR is non empty by S1;
then x' in cR;
then x' in union C by EQREL_1:def 6;
then consider y being set such that
B1: x in y and
C1: y in C by TARSKI:def 4;
take y;
thus thesis by A1, B1, C1;
end;
consider f being Function of A, C such that
Q: for x being set st x in A holds P[x,f.x] from FUNCT_2:sch 1(P);
take f;
R: f is one-to-one proof
let x1,x2 be set such that
A1: x1 in dom f and
B1: x2 in dom f and
C1: f.x1 = f.x2;
F1: x1 in f.x1 by A1, Q;
G1: x2 in f.x2 by B1, Q;
f.x1 in C by S1, A1, FUNCT_2:7;
then f.x1 is Clique of R by LCpart;
hence x1 = x2 by A1, B1, F1, G1, C1, ACClique;
end;
C is finite by A;
then rng f = C by A, R, FINSEQ_4:78;
then f is onto by FUNCT_2:def 3;
hence f is bijective by R;
let x be set;
assume x in A;
hence x in f.x by Q;
end;
end;
theorem ACpart2: :: 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
A: card C = card A;
consider f being Function of A, C such that
B: f is bijective and
C: for x being set st x in A holds x in f.x by A, ACpart1;
let c be set such that
D: c in C;
rng f = C by B, FUNCT_2:def 3;
then consider x being set such that
E: x in dom f and
F: c = f.x by D, FUNCT_1:def 5;
G: x in c by E, F, C;
reconsider a = x as Element of A by E;
take a;
now
let z be set;
hereby
assume z in c /\ A;
then A1: z in c & z in A by XBOOLE_0:def 4;
c is Clique of R by D, LCpart;
hence z = a by A1, G, ACClique;
end;
assume z = a;
hence z in c /\ A by G, E, XBOOLE_0:def 4;
end;
hence c /\ A = {a} by TARSKI:def 1;
end;
theorem Main: :: 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
B1: card U = stability# R and
C1: card L = stability# R;
D1: 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;
S2d: aA = the carrier of Pa by YELLOW_0:def 15;
S2e: 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 D1;
A /\ Upper A = A by XBOOLE_1:21;
then D1a: A is StableSet of Pa by SPAChain;
consider f being Function of A, U such that
E1: f is bijective and
E1a: for x being set st x in A holds x in f.x by A1, B1, D1a, ACpart1;
E1b: dom f = A by D1, FUNCT_2:def 1;
E1d: rng f = U by E1, FUNCT_2:def 3;
reconsider Pb = subrelstr Lower A as
with_finite_stability# antisymmetric transitive non empty RelStr by D1;
A /\ Lower A = A by XBOOLE_1:21;
then F1a: A is StableSet of Pb by SPAChain;
consider g being Function of A, L such that
G1: g is bijective and
G1a: for x being set st x in A holds x in g.x by A1, C1, F1a, ACpart1;
G1b: dom g = A by D1, FUNCT_2:def 1;
G1d: rng g = L by G1, FUNCT_2:def 3;
set h = f .\/ g; set C = rng h;
I1a: dom h = dom f \/ dom g by LEXBFS:def 2;
Y1a: C c= bool cR proof
let x be set;
assume x in C;
then consider a being set such that
A2: a in dom h and
B2: h.a = x by FUNCT_1:def 5;
C2: h.a = f.a \/ g.a by A2, I1a, LEXBFS:def 2;
f.a in U by A2, I1a, FUNCT_2:7;
then D2: f.a c= cR by S2d, XBOOLE_1:1;
g.a in L by A2, I1a, FUNCT_2:7;
then g.a c= cR by S2e, XBOOLE_1:1;
then x c= cR by B2, C2, D2, XBOOLE_1:8;
hence x in bool cR;
end;
Y1b: union C = cR proof
now let x be set;
hereby assume x in union C;
then consider Y being set such that
B2: x in Y and
C2: Y in C by TARSKI:def 4;
consider a being set such that
D2: a in dom h and
E2: Y = h.a by C2, FUNCT_1:def 5;
F2: x in f.a \/ g.a by D2, E2, B2, I1a, LEXBFS:def 2;
per cases by F2, XBOOLE_0:def 3;
suppose S2: x in f.a;
f.a in U by D2, I1a, FUNCT_2:7;
then x in aA by S2, S2d;
hence x in cR;
end;
suppose S2: x in g.a;
g.a in L by D2, I1a, FUNCT_2:7;
then x in bA by S2, S2e;
hence x in cR;
end;
end;
assume x in [#]R;
then A2: x in Upper A \/ Lower A by A1, ABunion;
per cases by A2, XBOOLE_0:def 3;
suppose x in Upper A;
then x in union U by S2d, EQREL_1:def 6;
then consider Y being set such that
A3: x in Y and
B3: Y in U by TARSKI:def 4;
consider a being set such that
C3: a in dom f and
D3: Y = f.a by B3, E1d, FUNCT_1:def 5;
E3: h.a in rng h by C3, I1a, E1b, G1b, FUNCT_1:12;
h.a = f.a \/ g.a by C3, I1a, E1b, G1b, LEXBFS:def 2;
then x in h.a by A3, D3, XBOOLE_0:def 3;
hence x in union C by E3, TARSKI:def 4;
end;
suppose x in Lower A;
then x in union L by S2e, EQREL_1:def 6;
then consider Y being set such that
A3: x in Y and
B3: Y in L by TARSKI:def 4;
consider a being set such that
C3: a in dom g and
D3: Y = g.a by B3, G1d, FUNCT_1:def 5;
E3: h.a in rng h by C3, I1a, E1b, G1b, FUNCT_1:12;
h.a = f.a \/ g.a by C3, I1a, E1b, G1b, LEXBFS:def 2;
then x in h.a by A3, D3, XBOOLE_0:def 3;
hence x in union C by E3, TARSKI:def 4;
end;
end;
hence thesis by TARSKI:2;
end;
Y1c: now
let a be Subset of cR;
assume a in C;
then consider x being set such that
B2: x in dom h and
C2: h.x = a by FUNCT_1:def 5;
D2: h.x = f.x \/ g.x by B2, I1a, LEXBFS:def 2;
set cfx = f.x, cgx = g.x;
E2: cfx in U by B2, I1a, FUNCT_2:7;
then reconsider cfx as Subset of Pa;
E2g: cgx in L by B2, I1a, FUNCT_2:7;
then reconsider cgx as Subset of Pb;
cfx <> {} by E2, EQREL_1:def 6;
hence a <> {} by C2, D2;
let b be Subset of cR;
assume b in C;
then consider y being set such that
B2y: y in dom h and
C2y: h.y = b by FUNCT_1:def 5;
D2y: h.y = f.y \/ g.y by B2y, I1a, LEXBFS:def 2;
set cfy = f.y, cgy = g.y;
E2y: cfy in U by B2y, I1a, FUNCT_2:7;
then reconsider cfy as Subset of Pa;
E2yg: cgy in L by B2y, I1a, FUNCT_2:7;
then reconsider cgy as Subset of Pb;
assume FF2: a <> b;
F2a: cfx <> cfy by E1, FF2, C2, C2y, B2, B2y, I1a, E1b, FUNCT_1:def 8;
F2g: cgx <> cgy by G1, FF2, C2, C2y, B2, B2y, I1a, G1b, FUNCT_1:def 8;
assume a meets b;
then a /\ b <> {} by XBOOLE_0:def 7;
then consider z being set such that
F2b: z in a /\ b by XBOOLE_0:def 1;
G2: z in a by F2b, XBOOLE_0:def 4;
H2: z in b by F2b, XBOOLE_0:def 4;
set cfz = f.z, cgz = g.z;
per cases by G2, H2, C2, C2y, D2, D2y, 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 by XBOOLE_0:def 7;
hence contradiction by E2, E2y, F2a, EQREL_1:def 6;
end;
suppose S1: z in cfx & z in cgy;
C3: z in A by S1, S2d, S2e, ABAC0;
D3: z in f.z by S1, S2d, S2e, ABAC0, E1a;
E3: cfz in U by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cfz as Subset of Pa;
z in cfx /\ cfz by S1, D3, XBOOLE_0:def 4;
then cfz meets cfx by XBOOLE_0:def 7;
then cfz = cfx by E2, E3, EQREL_1:def 6;
then F3: z = x by E1, B2, C3, I1a, E1b, FUNCT_1:def 8;
D3g: z in g.z by S1, S2d, S2e, ABAC0, G1a;
E3g: cgz in L by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cgz as Subset of Pb;
z in cgz /\ cgy by S1, D3g, XBOOLE_0:def 4;
then cgz meets cgy by XBOOLE_0:def 7;
then cgz = cgy by E2yg, E3g, EQREL_1:def 6;
hence contradiction by F3, FF2, C2, C2y, G1, B2y,
C3, I1a, G1b, FUNCT_1:def 8;
end;
suppose S1: z in cgx & z in cfy;
C3: z in A by S1, S2d, S2e, ABAC0;
D3: z in f.z by S1, S2d, S2e, ABAC0, E1a;
E3: cfz in U by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cfz as Subset of Pa;
z in cfy /\ cfz by S1, D3, XBOOLE_0:def 4;
then cfz meets cfy by XBOOLE_0:def 7;
then cfz = cfy by E2y, E3, EQREL_1:def 6;
then F3: z = y by E1, B2y, C3, I1a, E1b, FUNCT_1:def 8;
D3g: z in g.z by S1, S2d, S2e, ABAC0, G1a;
E3g: cgz in L by S1, S2d, S2e, ABAC0, FUNCT_2:7;
then reconsider cgz as Subset of Pb;
z in cgz /\ cgx by S1, D3g, XBOOLE_0:def 4;
then cgz meets cgx by XBOOLE_0:def 7;
then cgz = cgx by E2g, E3g, EQREL_1:def 6;
hence contradiction by F3, FF2,C2,C2y, G1, B2, C3, I1a,
G1b, FUNCT_1:def 8;
end;
suppose z in cgx & z in cgy;
then z in cgx /\ cgy by XBOOLE_0:def 4;
then cgx meets cgy by XBOOLE_0:def 7;
hence contradiction by E2g, E2yg, F2g, EQREL_1:def 6;
end;
end;
Z1: 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 set such that
B2: x in dom h and
C2: c = h.x by FUNCT_1:def 5;
D2: c = f.x \/ g.x by B2, C2, I1a, LEXBFS:def 2;
set cf = f.x, cg = g.x;
cf in U by B2, I1a, FUNCT_2:7;
then
G2b: cf is Clique of Pa by LCpart;
then G2a: cf is Clique of R by SPClique;
cg in L by B2, I1a, FUNCT_2:7;
then
H2b: cg is Clique of Pb by LCpart;
then H2a: cg is Clique of R by SPClique;
then reconsider c' = c as Subset of R by D2, G2a, XBOOLE_1:8;
now let a, b being Element of R such that
A3: a in c' and
B3: b in c' and
C3: a <> b;
E3: x in cf by B2, I1a, E1a;
F3: x in cg by B2, I1a, G1a;
reconsider x as Element of R by B2, I1a, E1b, G1b;
per cases by A3, B3, D2, XBOOLE_0:def 3;
suppose a in f.x & b in f.x;
hence a <= b or b <= a by G2a, C3, DClique;
end;
suppose S1: a in f.x & b in g.x;
A4: x = a or x <= a by E3, S1, B2, I1a, G2b, PabSmin;
B4: x = b or b <= x by F3, S1, B2, I1a, H2b, PbeSmax;
thus a <= b or b <= a by C3, A4, B4, YELLOW_0:def 2;
end;
suppose S1: a in g.x & b in f.x;
A4: x = a or a <= x by F3, S1, B2, I1a, H2b, PbeSmax;
B4: x = b or x <= b by E3, S1, B2, I1a, G2b, PabSmin;
thus a <= b or b <= a by C3, A4, B4, YELLOW_0:def 2;
end;
suppose a in g.x & b in g.x;
hence a <= b or b <= a by H2a, C3, DClique;
end;
end;
hence c is Clique of R by DClique;
end;
H1: h is one-to-one proof
let x1,x2 be set such that
A2: x1 in dom h and
B2: x2 in dom h and
C2: h.x1 = h.x2;
D2: h.x1 is Clique of R by Z1, A2, FUNCT_1:12;
D2b: h.x1 = f.x1 \/ g.x1 by I1a, A2, LEXBFS:def 2;
x1 in f.x1 & x1 in g.x1 by A2, I1a, E1a, G1a;
then D2a: x1 in h.x1 by D2b, XBOOLE_0:def 3;
E2b: h.x2 = f.x2 \/ g.x2 by I1a, B2, LEXBFS:def 2;
x2 in f.x2 & x2 in g.x2 by B2, I1a, E1a, G1a;
then x2 in h.x2 by E2b, XBOOLE_0:def 3;
hence x1 = x2 by I1a, A2, B2, C2, D2, D2a, ACClique;
end;
reconsider C as Clique-partition of R
by Y1a, Y1b, Y1c, EQREL_1:def 6, Z1, LCpart;
take C;
card C = card h by H1, PRE_POLY:19
.= card A by I1a, E1b, G1b, CARD_1:104;
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
:LACpart:
for x being set st x in P holds x is StableSet of R;
end;
registration
let R be RelStr;
cluster StableSet-wise 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:54;
take S;
let x be set;
thus thesis;
end;
suppose S: R is non empty;
then reconsider RR = R as non empty RelStr;
take S = SmallestPartition cR;
let z being set;
assume A: z in S;
S = {{x} where x is Element of cR: not contradiction} by S, EQREL_1:46;
then consider x being Element of RR such that
W: z = {x} by A;
thus z is StableSet of R by W;
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 a_partition of the carrier of R;
coherence
proof let P be a_partition of the carrier of R;
let x be set;
thus thesis;
end;
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 A: card(C) < clique# R;
consider A being Clique of R such that
B: card A = clique# R by Lheight;
card card C = card C & card card A = card A;
then C: card C in card A by A, B, NAT_1:42;
set cR = the carrier of R;
per cases;
suppose S1: R is empty;
thus contradiction by A, S1;
end;
suppose S1: R is non empty;
defpred P[set,set] means
$1 in A & $2 in C & $1 in $2;
P: for x being set st x in A ex y being set st y in C & P[x,y] proof
let x be set such that
A1: x in A;
reconsider x' = x as Element of R by A1;
cR is non empty by S1;
then x' in cR;
then x in union C by EQREL_1:def 6;
then consider y being set such that
B1: x in y and
C1: y in C by TARSKI:def 4;
take y;
thus thesis by A1, B1, C1;
end;
consider f being Function of A, C such that
Q: for x being set st x in A holds P[x,f.x] from FUNCT_2:sch 1(P);
consider x,y being set such that
A1: x in A and
B1: y in A and
C1: x <> y and
D1: f.x = f.y by S1, C, FINSEQ_4:80;
f.x in C by A1, FUNCT_2:7;
then
E1: f.x is StableSet of R by LACpart;
x in f.x & y in f.x by D1, A1, B1, Q;
hence contradiction by E1, A1, B1, C1, ACClique;
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.
theorem DWf: :: 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;
P: for n being Nat st for k being Nat st k < n holds P[k] holds P[n] proof
let n be Nat; assume
A1: for k being Nat st k < n holds P[k];
let P be finite antisymmetric transitive RelStr; assume
B1: card(P) = n;
set wP = stability# P;
per cases;
suppose S1: n = 0;
then P is empty by B1;
then reconsider C = {} as Clique-partition of P by EQREL_1:54;
take C;
P is empty by B1, S1;
hence card(C) = stability# P by B1, S1;
end;
suppose S1: 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
S2a: card A = stability# P and
S2b: A <> minimals(P) and
S2c: 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 S1, B1;
S2d: aA = the carrier of Pa by YELLOW_0:def 15;
S2e: bA = the carrier of Pb by YELLOW_0:def 15;
not minimals PP c= aA by S2b, PCAmin, PCAamin;
then consider mi being set such that
A2a: mi in minimals P and
A2b: not mi in aA by TARSKI:def 3;
not maximals PP c= bA by S2c, PCAmax, PCAbmax;
then consider ma being set such that
B2a: ma in maximals P and
B2b: not ma in bA by TARSKI:def 3;
reconsider Pa as finite antisymmetric transitive RelStr;
mi in cP by A2a;
then aA c< cP by A2b, XBOOLE_0:def 8;
then card Pa < card P by S2d, CARD_2:67;
then consider Ca being Clique-partition of Pa such that
C2a: card(Ca) = stability# Pa by A1, B1;
C2b: stability# Pa = wP by S2a, Wsubp1, XBOOLE_1:7;
reconsider Pb as finite antisymmetric transitive RelStr;
ma in cP by B2a;
then bA c< cP by B2b, XBOOLE_0:def 8;
then card Pb < card P by S2e, CARD_2:67;
then consider L being Clique-partition of Pb such that
D2a: card(L) = stability# Pb by A1, B1;
D2b: stability# Pb = wP by S2a, Wsubp1, XBOOLE_1:7;
consider C being Clique-partition of P such that
Z: card C = stability# PP by S2a, C2a, C2b, D2a, D2b, Main;
take C;
thus card(C) = stability# P by Z;
end;
suppose S2: 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
B2: card(S) = stability# P by Lwidth;
reconsider PP = P as finite non empty antisymmetric transitive RelStr
by S1, B1;
set iR = the InternalRel of PP, cR = the carrier of PP;
consider a being Element of minimals(P);
D2a: a in minimals(PP);
reconsider a as Element of PP by D2a;
consider b being Element of PP such that
F2: b is_maximal_in [#]PP and
G2: a = b or a < b by Pminmax;
F2a: b in maximals(P) by F2, Lmax;
set cP = the carrier of P, cPP = the carrier of PP;
set Cn = {a, b}; set cP' = cP \ Cn;
G2a: cP = cP' \/ Cn by XBOOLE_1:45;
G2b: cP' misses {a,b} by XBOOLE_1:79;
then G2c: cP \ cP' = {a,b} by G2a, XBOOLE_1:88;
reconsider cP' as Subset of cR;
set P' = subrelstr cP';
H2a: cP' = the carrier of P' by YELLOW_0:def 15;
set k = card P';
H2: card cP'= card P' by YELLOW_0:def 15;
card cP' = card cP - card {a,b} by CARD_2:63;
then consider C being Clique-partition of P' such that
I2: card(C) = stability# P' by A1, B1, H2, XREAL_1:46;
I2a: not {a,b} in C proof
assume :: works through typing: Subset-Family -> Subset bool ...
A3: {a,b} in C;
B3: a in {a,b} by TARSKI:def 2;
thus contradiction by G2b, ZFMISC_1:55, H2a, A3, B3;
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:11;
then wP1 in NAT by INT_1:16;
then reconsider wP1 as Nat;
set S' = S /\ cP';
S /\ cP = S by XBOOLE_1:28;
then J2aa: S' = S \ {a,b} by XBOOLE_1:49;
J2ab: {a,b} = {a} \/ {b} by ENUMSET1:41;
reconsider S' as StableSet of P' by SPAChain;
J2a: card S' = wP1 proof
per cases by S2, B2;
suppose S3: S = minimals(P);
S' = S \ {a} proof
per cases;
suppose a = b;
hence S' = S \ {a} by J2aa, ENUMSET1:69;
end;
suppose A5aa: a <> b;
now
assume b in minimals(PP);
then b is_minimal_in [#]PP by Lmin;
hence contradiction by A5aa, G2, WAYBEL_4:57;
end;
hence S' = S \ {a} by J2aa, J2ab, S3, set00;
end;
end;
hence card S' = card S - card {a} by S3, EULER_1:5
.= wP1 by B2, CARD_1:50;
end;
suppose S3: S = maximals(PP);
A4: S' = S \ {b} proof
per cases;
suppose a = b;
hence S' = S \ {b} by J2aa, ENUMSET1:69;
end;
suppose A5aa: a <> b;
now
assume a in maximals(PP);
then a is_maximal_in [#]PP by Lmax;
hence contradiction by A5aa, G2, WAYBEL_4:56;
end;
hence S' = S \ {b} by J2aa, J2ab, S3, set00;
end;
end;
b in S by S3, F2, Lmax;
hence card S' = card S - card {b} by A4, EULER_1:5
.= wP1 by B2, CARD_1:50;
end;
end;
J2b: for T being StableSet of P' holds card(T) <= card(S') proof
let T be StableSet of P';
assume card(T) > card(S');
then card T >= card S' + 1 by NAT_1:13;
then consider V being StableSet of P' such that
B3: card V = card S' + 1 by AChain1;
C3: V is StableSet of P by SPAChain1;
V = minimals(P) or V =maximals(P) by S2,C3,B3,J2a;
hence contradiction by D2a, F2a, H2a, G2b, ZFMISC_1:55;
end;
J2c: stability# P' + 1 = wP - 1 + 1 by J2a,J2b,Lwidth .= wP;
set CC = C \/ {{a,b}};
cP' <> cP by G2c, XBOOLE_1:37;
then
x: cP' c< cP by XBOOLE_0:def 8;
now :: Cliques in CC
let x be set;
assume A3: x in CC;
per cases by A3, XBOOLE_0:def 3;
suppose x in C;
then x is Clique of P' by LCpart;
hence x is Clique of P by SPClique;
end;
suppose x in {{a,b}};
then A4: x = {a,b} by TARSKI:def 1;
per cases;
suppose a = b;
then x = {a} by A4, ENUMSET1:69;
hence x is Clique of P;
end;
suppose a <> b;
then a <= b by G2, ORDERS_2:def 10;
hence x is Clique of P by A4, Clique36b;
end;
end;
end;
then reconsider CC as Clique-partition of P by G2c, H2a, SPpart,LCpart,x;
take CC;
thus card(CC) = stability# P by I2, J2c, I2a, CARD_2:54;
end;
end;
end;
Z: for n being Nat holds P[n] from NAT_1:sch 4(P);
let R be finite antisymmetric transitive RelStr;
card R = card R;
hence thesis by Z;
end;
definition
let R be with_finite_stability# non empty RelStr, C be Subset of R;
attr C is strong-chain means :Lsc:
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 Subset of R;
coherence
proof
let C be Subset of R;
assume A: C is strong-chain;
now
let a, b be Element of R such that
A1: a in C and
B1: b in C and
B1a: 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
C1: 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 A, Lsc;
consider c being set such that
D1: c in P and
E1: S /\ C c= c and
for d being set st d in P & d <> c holds C /\ d = {} by C1;
c is Clique of subrelstr S by D1, LCpart;
then F1: c is Clique of R by SPClique;
a in S & b in S by TARSKI:def 2;
then a in S /\ C & b in S /\ C by A1, B1, XBOOLE_0:def 4;
hence a <= b or b <= a by E1, F1, B1a, DClique;
end;
hence C is clique by DClique;
end;
end;
registration
let R be with_finite_stability# antisymmetric transitive non empty RelStr;
cluster trivial non empty -> strong-chain Subset of R;
coherence
proof
let C be Subset of R;
assume C is trivial non empty;
then consider x being set such that
Z: C = {x} by REALSET1:def 4;
let S be finite non empty Subset of R;
consider P being Clique-partition of subrelstr S such that
A1: card P = stability# subrelstr S by DWf;
cS: S = the carrier of subrelstr S by YELLOW_0:def 15;
take P;
thus card P <= stability# R by A1, Wsubp0;
per cases;
suppose x in S;
then x in union P by cS, EQREL_1:def 6;
then consider c being set such that
A2: x in c and
B2: c in P by TARSKI:def 4;
take c;
thus c in P by B2;
thus S /\ C c= c proof
let a be set;
assume a in S /\ C;
then a in C by XBOOLE_0:def 4;
hence thesis by A2, Z,TARSKI:def 1;
end;
let d be set such that
C3: d in P and
D3: d <> c;
assume C /\ d <> {};
then consider a being set such that
E3: a in C /\ d by XBOOLE_0:def 1;
reconsider d, c as Subset of S by C3, B2, YELLOW_0:def 15;
a in C by E3, XBOOLE_0:def 4;
then a = x by Z,TARSKI:def 1;
then x in d by E3, XBOOLE_0:def 4;
then x in d /\ c by A2, XBOOLE_0:def 4;
then d meets c by XBOOLE_0:def 7;
hence contradiction by C3, B2, D3, EQREL_1:def 6;
end;
suppose S1: not x in S;
consider c being Element of P;
take c;
thus c in P;
C misses S by S1, ZFMISC_1:56,Z;
then S /\ C = {} by XBOOLE_0:def 7;
hence S /\ C c= c by XBOOLE_1:2;
let d be set such that
A2: d in P and d <> c;
not x in d by S1, cS, A2;
then C misses d by ZFMISC_1:56,Z;
hence C /\ d = {} by XBOOLE_0:def 7;
end;
end;
end;
theorem Maxsc: :: 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 };
consider x being Element of R;
reconsider xs = {x} as Subset of R;
Aa: {x} in E;
now :: premise of maximal principle
let Z be set such that
A1: Z c= E and
B1: Z is c=-linear;
set Y = union Z;
take Y;
now
let B be set;
assume B in Z;
then B in E by A1;
then ex C being Subset of R st C = B & C is strong-chain;
hence B c= the carrier of R;
end;
then reconsider Y' = Y as Subset of R by ZFMISC_1:94;
Y' is strong-chain proof
let S be finite non empty Subset of R;
set F = S /\ Y;
per cases;
suppose S1: F is empty;
consider p being Clique-partition of subrelstr S such that
A3: card p = stability# subrelstr S by DWf;
take p;
thus card p <= stability# R by Wsubp0, A3;
consider c being Element of p;
take c;
thus c in p;
thus S /\ Y' c= c by S1, XBOOLE_1:2;
let d be set such that
B3: d in p and d <> c;
d c= the carrier of subrelstr S by B3;
then d c= S by YELLOW_0:def 15;
hence Y' /\ d = {} by S1, XBOOLE_1:26, XBOOLE_1:3;
end;
suppose S1: F is non empty;
S1a: Z is non empty by S1, ZFMISC_1:2;
defpred P[set,set] means
$1 in F & $2 in Z & $1 in $2;
P: for x being set st x in F ex y being set st y in Z & P[x,y] proof
let x be set;
assume A4a: x in F;
then x in Y by XBOOLE_0:def 4;
then consider y being set such that
A4: x in y and
B4: y in Z by TARSKI:def 4;
take y;
thus thesis by B4, A4a, A4;
end;
consider f being Function of F, Z such that
J3: for x being set st x in F holds P[x,f.x] from FUNCT_2:sch 1(P);
set rf = rng f;
l3: rf c= Z & Z is c=-linear implies rf is c=-linear;
consider m being set such that
M3: m in rf and
N3: for C being set st C in rf holds C c= m
by l3, B1, RELAT_1:def 19, FINSET_1:31, S1, S1a;
rf c= Z by RELAT_1:def 19;
then m in Z by M3;
then m in E by A1;
then consider C being Subset of R such that
O3: m = C and
P3: C is strong-chain;
P3a: F c= C proof
let x be set;
assume A4: x in F;
then B4: x in f.x by J3;
f.x c= C by O3, N3, A4, S1a, FUNCT_2:6;
hence x in C by B4;
end;
consider p being Clique-partition of subrelstr S such that
R3: card p <= stability# R and
S3: 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 P3, Lsc;
take p;
thus card p <= stability# R by R3;
consider c being set such that
T3: c in p and
U3: S /\ C c= c and
V3: for d being set st d in p & d <> c holds C /\ d = {} by S3;
take c;
thus c in p by T3;
thus S /\ Y' c= c proof
let x be set;
assume x in S /\ Y';
then x in S & x in C by P3a, XBOOLE_0:def 4;
then x in S /\ C by XBOOLE_0:def 4;
hence x in c by U3;
end;
let d be set such that
W3: d in p and
X3: d <> c;
assume Y' /\ d <> {};
then consider x being set such that
Y3: x in Y' /\ d by XBOOLE_0:def 1;
Y3a: x in Y' by Y3, XBOOLE_0:def 4;
Z3: x in d by Y3, XBOOLE_0:def 4;
d is Subset of S by W3, YELLOW_0:def 15;
then x in F by Z3, Y3a, XBOOLE_0:def 4;
then x in C /\ d by Z3, P3a, XBOOLE_0:def 4;
hence contradiction by W3, X3, V3;
end;
end;
hence Y in E;
let X1 be set such that
C1: X1 in Z;
thus X1 c= Y by C1, ZFMISC_1:92;
end;
then consider Y being set such that
B: Y in E and
C: for Z being set st Z in E & Z <> Y holds not Y c= Z by Aa, ORDERS_1:175;
consider C being Subset of R such that
D: Y = C and
E: C is strong-chain by B;
reconsider S = C as non empty Subset of R by D, Aa, C, XBOOLE_1:2;
take S;
thus S is strong-chain by E;
let D be Subset of R such that
F: D is strong-chain and
G: S c< D;
I: D in E by F;
D <> S & S c= D by G, XBOOLE_0:def 8;
hence contradiction by D, I, C;
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 DWf;
end;
suppose S0: 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;
P1: P[0];
P2: for k be Nat st P[k] holds P[k + 1] proof
let k be Nat;
assume A: P[k];
let P be with_finite_stability# non empty antisymmetric transitive RelStr;
assume B: stability# P = k+1;
consider C being non empty Subset of P such that
C: C is strong-chain and
D: not ex D being Subset of P st D is strong-chain & C c< D by Maxsc;
set cP = the carrier of P;
per cases;
suppose S1: C = cP; :: real base case
for x being set st x in { C } holds x is Clique of P
by C, TARSKI:def 1;
then reconsider Cp = { C } as Clique-partition of P
by LCpart,S1,EQREL_1:48;
take Cp;
R: cP = [#]P;
thus card Cp = 1 by CARD_1:50
.= stability# P by R, C, S1, Width3;
end;
suppose C <> cP;
then S1a: C c< cP by XBOOLE_0:def 8;
set cP' = cP \ C;
E: cP \ cP' = cP /\ C by XBOOLE_1:48
.= C by XBOOLE_1:28;
reconsider cP' as Subset of P;
set P' = subrelstr cP';
cP' <> {} by S1a, XBOOLE_1:105;
then reconsider P' = subrelstr cP'
as with_finite_stability# non empty antisymmetric transitive RelStr;
cP'c: cP' = the carrier of P' by YELLOW_0:def 15;
G: stability# P' <= k+1 by B, Wsubp0;
H: stability# P' <> k+1 proof
assume AA: stability# P' = k+1;
consider A being finite StableSet of P' such that
A1: card(A) = stability# P' by Lwidth;
reconsider A' = A as finite non empty StableSet of P by A1, SPAChain1;
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[set,set] means
ex S being finite non empty Subset of P
st $2 = S & $1 in $2 & Q[S, C\/{$1}];
P: for x being set st x in A ex y being set st P[x,y] proof
let a be set;
assume A2: a in A;
A c= cP by cP'c, XBOOLE_1:1;
then {a} c= cP by A2, ZFMISC_1:37;
then reconsider Ca = C \/ {a} as Subset of P by XBOOLE_1:8;
now
assume A3: Ca is strong-chain;
a in {a} by TARSKI:def 1;
then B3: a in Ca by XBOOLE_0:def 3;
C3: not a in C by cP'c, A2, XBOOLE_0:def 5;
C c= Ca by XBOOLE_1:7;
then C c< Ca by B3, C3, XBOOLE_0:def 8;
hence contradiction by A3, D;
end;
then consider S being finite non empty Subset of P such that
B2: Q[S,Ca] by Lsc;
take S;
take S;
thus S = S;
now
assume A3: not a in S;
A3b: S /\ C c= S /\ Ca proof
let x be set;
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 set;
assume A4: x in S /\ Ca;
then B4: x in S by XBOOLE_0:def 4;
x in Ca by A4, XBOOLE_0:def 4;
then x in C or x in {a} by XBOOLE_0:def 3;
hence x in S /\ C by B4, A3, TARSKI:def 1, XBOOLE_0:def 4;
end;
then A3a: S /\ C = S /\ Ca by A3b, XBOOLE_0:def 10;
consider p being Clique-partition of subrelstr S such that
B3: card p <= stability# P and
C3: not R[S,p,C] by C, Lsc;
consider c being set such that
D3: c in p and
E3: S /\ C c= c and
F3: for d being set st d in p & d <> c holds C /\ d = {} by C3;
for d being set st d in p & d <> c holds Ca /\ d = {} proof
let d be set such that
A4: d in p and
B4: d <> c;
now
assume Ca /\ d <> {};
then consider x being set such that
A5: x in Ca /\ d by XBOOLE_0:def 1;
B5: x in Ca by A5, XBOOLE_0:def 4;
C5: x in d by A5, XBOOLE_0:def 4;
per cases by B5, XBOOLE_0:def 3;
suppose x in C;
then x in C /\ d by C5, XBOOLE_0:def 4;
hence contradiction by A4, B4, F3;
end;
suppose x in {a};
then x = a by TARSKI:def 1;
then a in the carrier of subrelstr S by C5, A4;
hence contradiction by A3, YELLOW_0:def 15;
end;
end;
hence Ca /\ d = {};
end;
hence contradiction by D3, E3, B3, A3a, B2;
end;
hence a in S;
thus thesis by B2;
end;
consider f being Function such that
C1: dom f = A and
E1: for x being set st x in A holds P[x,f.x] from CLASSES1:sch 1(P);
D1a: rng f is finite by C1, FINSET_1:26;
set SS = union rng f;
C1bb: 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 set such that
A2: a in dom f and
B2: x = f.a by FUNCT_1:def 5;
consider S being finite non empty Subset of P such that
C2: f.a = S and a in f.a & Q[S, C \/ {a}] by C1, A2, E1;
thus x is finite by C2, B2;
end;
C1c: SS c= cP proof
let x be set;
assume x in SS;
then consider y being set such that
A2: x in y and
B2: y in rng f by TARSKI:def 4;
consider a being set such that
C2: a in dom f and
D2: y = f.a by B2, FUNCT_1:def 5;
consider S being finite non empty Subset of P such that
E2: f.a = S and a in f.a & Q[S, C \/ {a}] by C1, C2, E1;
thus x in cP by A2, D2, E2;
end;
C1a: A' c= SS proof
let x be set;
assume A2: x in A';
then consider S being finite non empty Subset of P such that
f.x = S and
D2: x in f.x and Q[S, C \/ {x}] by E1;
f.x in rng f by A2, C1, FUNCT_1:12;
hence x in SS by D2, TARSKI:def 4;
end;
then reconsider SS as finite non empty Subset of P
by C1bb, D1a, FINSET_1:25, C1c;
set SSp = subrelstr SS;
cSS: SS = the carrier of SSp by YELLOW_0:def 15;
consider p being Clique-partition of SSp such that
F1: card p <= stability# P and
G1: not R[SS,p,C] by C, Lsc;
consider c being set such that
H1: c in p and
I1: SS /\ C c= c and
J1: for d being set st d in p & d <> c holds C /\ d = {} by G1;
reconsider c as Element of p by H1;
A' = A' /\ SS by C1a, XBOOLE_1:28;
then reconsider A = A' as finite non empty StableSet of SSp by SPAChain;
K1: stability# SSp >= card A by Lwidth;
card p >= stability# SSp by Chpw;
then card p >= card A by K1, XXREAL_0:2;
then consider a being Element of A such that
L1: c /\ A = {a} by ACpart2, F1, A1, AA, B, XXREAL_0:1;
a in c /\ A by L1, TARSKI:def 1; then
M1: a in c by XBOOLE_0:def 4;
consider S being finite non empty Subset of P such that
N1: f.a = S and
O1: a in f.a and
P1: Q[S, C \/ {a}] by E1;
deffunc F(set) = $1 /\ S;
defpred P[set] means $1 meets S;
set Sp = { F(e) where e is Element of p: P[e]};
R1: S c= SS proof
let x be set;
assume A2: x in S;
S in rng f by N1, C1, FUNCT_1:12;
hence x in SS by A2, TARSKI:def 4;
end;
then reconsider Sp as a_partition of S by cSS, 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
A2: x = e /\ S and e meets S;
e is Clique of SSp by LCpart;
then e is Clique of P by SPClique;
hence x is Clique of subrelstr S by A2, SPClique1;
end;
then reconsider Sp as Clique-partition of subrelstr S
by YELLOW_0:def 15, LCpart;
T1a: Sp = { F(e) where e is Element of p: P[e]};
T1b: card Sp <= card p from FraenkelFinCard1(T1a);
set cc = c /\ S;
c meets S by M1, N1, O1, XBOOLE_0:3; then
U1: cc in Sp;
S /\ (C \/ {a}) c= cc proof
let x be set;
assume A2: x in S /\ (C \/ {a});
B2: x in S by A2, XBOOLE_0:def 4;
C2: x in C \/ {a} by A2, XBOOLE_0:def 4;
per cases by C2, XBOOLE_0:def 3;
suppose x in C;
then x in SS /\ C by B2, R1, XBOOLE_0:def 4;
hence x in cc by B2, I1, XBOOLE_0:def 4;
end;
suppose x in {a};
then x = a by TARSKI:def 1;
hence x in cc by M1, N1, O1, XBOOLE_0:def 4;
end;
end;
then consider d being set such that
V1: d in Sp and
W1: d <> cc and
X1: (C \/ {a}) /\ d <> {} by U1, T1b, F1, XXREAL_0:2, P1;
consider dd being Element of p such that
Y1: d = dd /\ S and
dd meets S by V1;
C /\ dd = {} by Y1, W1, J1; then
Z1a: C /\ d = {} /\ S by Y1, XBOOLE_1:16 .= {};
C /\ d \/ {a} /\ d <> {} by X1, XBOOLE_1:23;
then consider x being set such that
Y1a: x in {a} /\ d by Z1a, XBOOLE_0:def 1;
x in {a} & x in d by Y1a, XBOOLE_0:def 4;
then a in d by TARSKI:def 1;
then a in dd by Y1, XBOOLE_0:def 4;
then c meets dd by M1, XBOOLE_0:3;
hence contradiction by Y1, W1, EQREL_1:def 6;
end;
then stability# P' < k+1 by G, XXREAL_0:1; then
Ha: stability# P' <= k by NAT_1:13;
consider A being finite StableSet of P such that
I: card A = stability# P by Lwidth;
Y: stability# P' = k proof
per cases;
suppose S2: A /\ C = {};
A c= cP' proof
let x be set;
assume A3: x in A;
not x in C by A3, S2, XBOOLE_0:def 4;
hence x in cP' by A3, XBOOLE_0:def 5;
end;
hence thesis by B, H, I, Wsubp1;
end;
suppose A /\ C <> {};
then consider x being set such that
A3: x in A /\ C by XBOOLE_0:def 1;
B3: x in A by A3, XBOOLE_0:def 4;
C3: x in C by A3, XBOOLE_0:def 4;
set A' = A \ {x};
{x} c= A by B3, ZFMISC_1:37;
then D3: A = A' \/ {x} by XBOOLE_1:45;
x in {x} by TARSKI:def 1;
then not x in A' by XBOOLE_0:def 5;
then D4a: card A = card A' + 1 by D3, CARD_2:54;
E4: A' c= A by XBOOLE_1:36;
A' c= cP' proof
let xx be set;
assume A5: xx in A';
B5: xx in A by A5, XBOOLE_0:def 5;
C5: not xx in {x} by A5, XBOOLE_0:def 5;
xx <> x by C5, TARSKI:def 1;
then not xx in C by B3, C3, B5, C, ACClique;
hence xx in cP' by A5, XBOOLE_0:def 5;
end; then
F4: A' c= A /\ cP' by E4, XBOOLE_1:19;
A /\ cP' c= A' proof
let xx be set;
assume A5: xx in A /\ cP';
B5: xx in A by A5, XBOOLE_0:def 4;
xx in cP' by A5, XBOOLE_0:def 4;
then x <> xx by C3, XBOOLE_0:def 5;
then not xx in {x} by TARSKI:def 1;
hence xx in A' by B5, XBOOLE_0:def 5;
end;
then A' = A /\ cP' by F4, XBOOLE_0:def 10;
then reconsider A' as StableSet of P' by SPAChain;
stability# P' >= card A' by Lwidth;
hence thesis by D4a, I, B, Ha, XXREAL_0:1;
end;
end;
then consider Cp' being Clique-partition of P' such that
Z: card(Cp') = stability# P' by A;
set Cp = Cp' \/ { cP \ cP' };
Zk: Cp' is finite by Z;
cP' <> cP by E, XBOOLE_1:37;
then
Zl: cP' c< cP by XBOOLE_0:def 8;
then reconsider Cp as a_partition of cP by cP'c, SPpart;
now :: chains in Cp;
let x be set;
assume A2: x in Cp;
per cases by A2, XBOOLE_0:def 3;
suppose x in Cp';
then x is Clique of P' by LCpart;
hence x is Clique of P by SPClique;
end;
suppose x in { cP \ cP' };
hence x is Clique of P by C,E, TARSKI:def 1;
end;
end;
then reconsider Cp as Clique-partition of P by LCpart;
take Cp;
not cP \ cP' in Cp' proof
assume not thesis;
then cP c= cP' \/ cP' by cP'c, XBOOLE_1:44;
hence contradiction by Zl, XBOOLE_1:60;
end;
hence card Cp = stability# P by B, Y, Z, Zk, CARD_2:54;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(P1,P2);
hence thesis by S0;
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;
P1: P[0] proof
let P be with_finite_clique# antisymmetric transitive RelStr;
assume S1a: clique# P = 0;
then P is empty;
then reconsider C = {} as Coloring of P by EQREL_1:54;
take C;
thus card(C) = clique# P by S1a;
end;
P2: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
assume AA: P[n];
let P be with_finite_clique# antisymmetric transitive RelStr;
assume A1: clique# P = n+1;
A1a: P is non empty by A1;
reconsider PP = P
as with_finite_clique# non empty antisymmetric transitive RelStr by A1;
set M = maximals(PP);
set cP = the carrier of P;
set cPM = cP \ M;
reconsider cPM as Subset of P;
set PM = subrelstr cPM;
cPM: 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
B1a: card Ca = clique# PM by Lheight;
C1b: Ca is Clique of P by SPClique;
consider C being finite Clique of P such that
B1: card(C) = n+1 by A1, Lheight;
B1b: C <> {} by B1;
set cC = C /\ cPM;
reconsider cC as finite Clique of PM by SPClique1;
consider m being Element of P such that
F1: m in C and
G1: m is_maximal_wrt C, the InternalRel of P by A1a, B1b, BAGORDER:7;
G1a: m is_maximal_in C by G1, WAYBEL_4:def 25;
H1: C /\ M = {m} proof
thus C /\ M c= {m} proof
let a be set;
assume A2: a in C /\ M;
B2: a in C by A2, XBOOLE_0:def 4;
C2: a in M by A2, XBOOLE_0:def 4;
reconsider a' = a as Element of P by A2;
D2: a' is_maximal_in [#]P by C2, Lmax;
now
assume A3: a <> m;
not m < a' by B2, G1a, WAYBEL_4:56;
then not m <= a' by A3, ORDERS_2:def 10;
then a' <= m by F1, B2, A3, DClique;
then a' < m by A3, ORDERS_2:def 10;
hence contradiction by D2, F1, WAYBEL_4:56;
end;
hence a in {m} by TARSKI:def 1;
end;
thus {m} c= C /\ M proof
let a be set;
assume a in {m};
then A2: a = m by TARSKI:def 1;
now
assume A3: not a in M;
consider y being Element of P such that
B3: y is_maximal_in [#]P and
C3: m = y or m < y by A1a, Pminmax;
set Cm = C \/ {y};
now
per cases;
suppose m = y;
hence Cm is finite Clique of P by F1, ZFMISC_1:46;
end;
suppose m <> y;
then m <= y by C3, ORDERS_2:def 10;
hence Cm is finite Clique of P by G1a, ExtClique;
end;
end;
then reconsider Cm as finite Clique of P;
not y in C by A2, A3, B3, Lmax, C3, G1a, WAYBEL_4:56;
then card Cm = card C + 1 by CARD_2:54;
then n+1+1 <= n+1+0 by B1, A1, Lheight;
hence contradiction by XREAL_1:8;
end;
hence a in C /\ M by A2, F1, XBOOLE_0:def 4;
end;
end;
D1b: cC = C /\ cP \ C /\ M by XBOOLE_1:50;
D1c: C /\ cP = C by XBOOLE_1:28;
D1: card cC = card C - card {m} by F1, H1, D1b, D1c, EULER_1:5
.= n+1-1 by B1, CARD_1:50
.= n;
D1a: clique# PM >= card cC by Lheight;
E1: clique# PM <= clique# P by Hsubp0;
now
assume A2: clique# PM = n+1;
B2: Ca <> {} by A2, B1a;
B2a:PM is non empty by A2;
consider x being Element of PM such that
D2e: x in Ca and
D2: x is_maximal_wrt Ca, the InternalRel of PM by B2a, B2, BAGORDER:7;
D2a: x is_maximal_in Ca by D2, WAYBEL_4:def 25;
reconsider x' = x as Element of P by B2a, YELLOW_0:59;
consider y being Element of P such that
E2: y is_maximal_in [#]P and
F2: x' = y or x' < y by Pminmax;
set Cb = Ca \/ {y};
now
per cases;
suppose x' = y;
hence Cb is finite Clique of P by D2e, C1b, ZFMISC_1:46;
end;
suppose x' <> y;
then x' <= y by F2, ORDERS_2:def 10;
hence Cb is finite Clique of P by D2a, SPmax, C1b, ExtClique;
end;
end;
then reconsider Cb as finite Clique of P;
y in M by E2, Lmax;
then not y in Ca by cPM, XBOOLE_0:def 5; then
G2: card Cb = n+1+1 by B1a, A2, CARD_2:54;
card Cb <= n+1 by A1, Lheight;
then n+1 <= n+0 by G2, XREAL_1:8;
hence contradiction by XREAL_1:8;
end;
then clique# PM < n+1 by A1, E1, XXREAL_0:1;
then clique# PM <= n by NAT_1:13;
then clique# PM = n by D1, D1a, XXREAL_0:1;
then consider Aa being Coloring of PM such that
K1: card Aa = n by AA;
reconsider Ab = Aa as finite set by K1;
set A = Aa \/ {M};
L1b: cP = cPM \/ M by XBOOLE_1:45;
{M} is a_partition of M by EQREL_1:48;
then
L1: A is a_partition of cP by XBOOLE_1:79, L1b, cPM, SPpart0;
now let x be set;
assume A2: x in A;
per cases by A2, XBOOLE_0:def 3;
suppose x in Aa;
then x is StableSet of PM by LACpart;
hence x is StableSet of P by SPAChain1;
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 L1, LACpart;
take A;
not M in Ab by cPM, XBOOLE_1:38;
hence card A = clique# P by A1, K1, CARD_2:54;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence ex A being Coloring of R st card(A) = clique# R;
end;
begin :: Erdos-Szekeres theorem
theorem CSR: :: 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
A: card R = r*s+1 and
B: for C being Clique of R holds card C < r+1 and
C: for A being StableSet of R holds card A < s+1;
consider p being Clique-partition of R such that
D: card p = stability# R by DWf;
consider A being finite StableSet of R such that
E: card A = stability# R by Lwidth;
stability# R < s+1 by C, E; then
Fa: stability# R <= s by NAT_1:13;
set wR = stability# R; set cR = the carrier of R; set f = canFS p;
Fb: len f = card p by UPROOTS:5;
Fd: dom f = Seg len f by FINSEQ_1:def 3;
set f = canFS p;
G: rng f = p by FUNCT_2:def 3;
reconsider f as FinSequence of bool cR by G, FINSEQ_1:def 4;
now
let d,e be Nat such that
A2: d in dom f and
B2: e in dom f and
C2: d<>e;
D2: f.d in rng f by A2, FUNCT_1:12;
E2: f.e in rng f by B2, FUNCT_1:12;
reconsider fd = f.d, fe = f.e as Subset of cR by D2, E2, G;
fd <> fe by C2, A2, B2, FUNCT_1:def 8;
hence f.d misses f.e by D2, E2, G, EQREL_1:def 6;
end;
then
I: card union rng f = Sum Card f by Fb, INT_5:48;
reconsider n' = r as Element of NAT by ORDINAL1:def 13;
reconsider h = wR |-> n' as Element of wR-tuples_on NAT by FINSEQ_2:132;
Ia: Sum h = wR*r by RVSUM_1:110;
dom f = dom Card f by CARD_3:def 2;
then
Ib: len Card f = wR by Fb, D, FINSEQ_3:31;
reconsider Cf = Card f as Element of wR-tuples_on NAT by Ib, FINSEQ_2:110;
Ic: h is Element of wR-tuples_on REAL by FINSEQ_2:129;
Ie: Cf is Element of wR-tuples_on REAL by FINSEQ_2:129;
now
let j being Nat such that
A2: j in Seg wR;
B2: h.j = r by A2, FINSEQ_2:71;
C2: Cf.j = card (f.j) by A2, Fb, Fd, D, CARD_3:def 2;
f.j in p by G,A2,D,Fb,Fd, FUNCT_1:12;
then
reconsider fj = f.j as Clique of R by LCpart;
card fj < r+1 by B;
hence Cf.j <= h.j by B2, C2, NAT_1:13;
end;
then
bI: Sum Cf <= Sum h by Ic, Ie, RVSUM_1:112;
wR*r <= s*r by Fa, XREAL_1:66;
then Sum Cf <= s*r by Ia, bI, XXREAL_0:2;
then r*s+1 <= r*s+0 by I, G, A, EQREL_1:def 6;
hence contradiction by XREAL_1:8;
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
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
A: card f = n^2+1 and
AA: f is one-to-one;
set cP = f;
defpred P[set,set] means
ex i,j being Nat, r, s being real number
st $1 = [i,r] & $2 = [j,s] & i= n+1;
then consider C being Clique of P such that
A1: 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 set;
assume x in dom g;
then consider y being set such that
A2: [x,y] in g by RELAT_1:def 4;
x in dom f by A2, RELAT_1:def 4;
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 A1;
g is increasing proof
let e1, e2 be ext-real number such that
A3: e1 in dom g and
B3: e2 in dom g and
C3: e1 < e2;
D3: [e1,g.e1] in g by A3, FUNCT_1:8;
E3: [e2,g.e2] in g by B3, FUNCT_1:8;
reconsider p1 = [e1,g.e1], p2 = [e2,g.e2] as Element of P by D3, E3;
F3: p1 <> p2 by C3, ZFMISC_1:33;
per cases by D3, E3, F3, DClique;
suppose p1 <= p2;
then [p1,p2] in iP by ORDERS_2:def 9;
then consider i,j being Nat, r, s being real number such that
A4: p1 = [i,r] and
B4: p2 = [j,s] and
C4: i= n+1;
then consider A being StableSet of P such that
A1: card A >= n+1;
set g = A;
reconsider g as Subset of f;
reconsider g as Function;
B1: dom g c= Seg len f proof
let x be set;
assume x in dom g;
then consider y being set such that
A2: [x,y] in g by RELAT_1:def 4;
x in dom f by A2, RELAT_1:def 4;
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 A1;
g is decreasing proof
let e1, e2 be ext-real number such that
A3: e1 in dom g and
B3: e2 in dom g and
C3: e1 < e2;
D3: [e1,g.e1] in g by A3, FUNCT_1:8;
E3: [e2,g.e2] in g by B3, FUNCT_1:8;
reconsider p1 = [e1,g.e1], p2 = [e2,g.e2] as Element of P by D3, E3;
F3: p1 <> p2 by C3, ZFMISC_1:33;
G3b: g.e1 = f.e1 & g.e2 = f.e2 by A3, B3, GRFUNC_1:8;
G3: g.e1 <> g.e2 by G3c, B1, A3, B3, G3b, C3, AA, FUNCT_1:def 8;
reconsider i = e1, j = e2 as Nat by B1, A3, B3;
reconsider r = g.e1, s = g.e2 as real number;
H3: p1 = [i,r] & p2 = [j,s];
per cases by G3, XXREAL_0:1;
suppose g.e1 < g.e2;
then [p1,p2] in iP by D3, B, C3, H3;
then p1 <= p2 by ORDERS_2:def 9;
hence g.e1 > g.e2 by D3, E3, F3, LAChain;
end;
suppose g.e1 > g.e2;
hence thesis;
end;
end;
hence thesis;
end;
end;