:: Dilworth's Decomposition Theorem for Posets :: by Piotr Rudnicki :: :: Received September 17, 2009 :: Copyright (c) 2009-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSET_1, XBOOLE_0, CARD_1, XXREAL_0, SUBSET_1, TARSKI, ORDINAL1, SETFAM_1, ZFMISC_1, EQREL_1, NAT_1, FUNCT_1, FINSEQ_1, ARYTM_3, RELAT_1, ORDERS_2, RELAT_2, COMBGRAS, STRUCT_0, ORDERS_1, CIRCUIT2, GROUP_10, RAMSEY_1, JORDAN4, WAYBEL_0, WAYBEL_4, YELLOW_0, FUNCT_2, LEXBFS, ARYTM_1, UPROOTS, CARD_3, FINSEQ_2, VALUED_0, SQUARE_1, ORDINAL2, DILWORTH, REAL_1; notations TARSKI, RELAT_1, RELAT_2, RELSET_1, FINSET_1, SETFAM_1, XBOOLE_0, SUBSET_1, CARD_1, STRUCT_0, WAYBEL_0, WAYBEL_4, ORDERS_2, ORDINAL1, EQREL_1, FUNCT_1, FUNCT_2, NUMBERS, XREAL_0, XXREAL_0, NAT_1, YELLOW_0, XCMPLX_0, ZFMISC_1, LEXBFS, FINSEQ_1, SQUARE_1, UPROOTS, RVSUM_1, INT_5, FINSEQ_2, VALUED_0, GROUP_10, RAMSEY_1, DOMAIN_1; constructors DOMAIN_1, LEXBFS, WAYBEL_4, SQUARE_1, UPROOTS, WSIERP_1, INT_5, RAMSEY_1, RELSET_1, BINOP_2, NUMBERS; registrations STRUCT_0, XXREAL_0, RELSET_1, CARD_1, YELLOW_0, XREAL_0, FINSET_1, XBOOLE_0, NAT_1, INT_1, YELLOW_2, EQREL_1, FINSEQ_1, FUNCT_1, SUBSET_1, ORDINAL1, PEPIN, RVSUM_1, FUNCT_2, FINSEQ_2, RELAT_1, VALUED_0, ORDERS_2; requirements ARITHM, SUBSET, BOOLE, NUMERALS, REAL; begin :: Preliminaries :: Facts that I could not find in MML. scheme :: DILWORTH:sch 1 FraenkelFinCard1 { A() -> finite non empty set, P[set], Y() -> finite set, F(set) -> set }: card Y() <= card A() provided Y() = { F(w) where w is Element of A(): P[w] }; theorem :: DILWORTH:1 :: set00: for X, Y, x being set st not x in X holds X \ (Y \/ {x}) = X \ Y; theorem :: DILWORTH:2 :: 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; theorem :: DILWORTH:3 :: 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; theorem :: DILWORTH:4 :: 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; theorem :: DILWORTH:5 :: Sinfset: for X being infinite set, n being Nat ex Y being finite Subset of X st card Y > n; begin :: Cliques and stable sets definition let R be RelStr, S be Subset of R; attr S is connected means :: DILWORTH:def 1 the InternalRel of R is_connected_in S; end; notation let R be RelStr, S be Subset of R; synonym S is clique for S is connected; end; registration let R be RelStr; cluster trivial -> clique for Subset of R; end; registration let R be RelStr; cluster clique for Subset of R; end; definition let R be RelStr; mode Clique of R is clique Subset of R; end; theorem :: DILWORTH:6 :: 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; registration let R be RelStr; cluster finite for Clique of R; end; registration let R be reflexive RelStr; cluster connected -> strongly_connected for Subset of R; end; registration let R be non empty RelStr; cluster finite non empty for Clique of R; end; theorem :: DILWORTH:7 :: 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; theorem :: DILWORTH:8 :: 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; theorem :: DILWORTH:9 :: Clique37: for R being RelStr, C being Clique of R, S being Subset of C holds S is Clique of R; theorem :: DILWORTH:10 :: Clique1: for R being RelStr, C being finite Clique of R, n being Nat st n <= card C ex B being finite Clique of R st B c= C & card B = n; theorem :: DILWORTH:11 :: 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; theorem :: DILWORTH:12 :: 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; definition let R be RelStr, S be Subset of R; attr S is stable means :: DILWORTH:def 2 for x, y being Element of R st x in S & y in S & x <> y holds not x <= y & not y <= x; end; registration let R be RelStr; cluster trivial -> stable for Subset of R; end; registration let R be RelStr; cluster stable for Subset of R; end; definition let R be RelStr; mode StableSet of R is stable Subset of R; :: other possible names: AntiChain of R, IndependentSet of R end; registration let R be RelStr; cluster finite for StableSet of R; end; registration let R be non empty RelStr; cluster finite non empty for StableSet of R; end; theorem :: DILWORTH:13 :: 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); theorem :: DILWORTH:14 :: 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; theorem :: DILWORTH:15 :: 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; theorem :: DILWORTH:16 :: AChain0: for R being RelStr, A being StableSet of R, B being Subset of A holds B is StableSet of R; theorem :: DILWORTH:17 :: 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; begin :: Clique number and stability number definition let R be RelStr; attr R is with_finite_clique# means :: DILWORTH:def 3 ex C being finite Clique of R st for D being finite Clique of R holds card D <= card C; end; registration cluster finite -> with_finite_clique# for RelStr; end; registration let R be with_finite_clique# RelStr; cluster -> finite for Clique of R; end; definition let R be with_finite_clique# RelStr; func clique# R -> Nat means :: DILWORTH:def 4 (ex C being finite Clique of R st card C = it) & for T being finite Clique of R holds card T <= it; end; registration let R be empty RelStr; cluster clique# R -> empty; end; registration let R be with_finite_clique# non empty RelStr; cluster clique# R -> positive; end; theorem :: DILWORTH:18 :: Height3: for R being with_finite_clique# non empty RelStr st [#]R is StableSet of R holds clique# R = 1; theorem :: DILWORTH:19 :: Height4: for R being with_finite_clique# RelStr st clique# R = 1 holds [#]R is StableSet of R; definition let R be RelStr; attr R is with_finite_stability# means :: DILWORTH:def 5 ex A being finite StableSet of R st for B being finite StableSet of R holds card B <= card A; end; registration cluster finite -> with_finite_stability# for RelStr; end; registration let R be with_finite_stability# RelStr; cluster -> finite for StableSet of R; end; definition let R be with_finite_stability# RelStr; func stability# R -> Nat means :: DILWORTH:def 6 (ex A being finite StableSet of R st card(A) = it) & for T being finite StableSet of R holds card T <= it; end; registration let R be empty RelStr; cluster stability# R -> empty; end; registration let R be with_finite_stability# non empty RelStr; cluster stability# R -> positive; end; theorem :: DILWORTH:20 :: Width3: for R being with_finite_stability# non empty RelStr st [#]R is Clique of R holds stability# R = 1; theorem :: DILWORTH:21 :: Width4: for R being with_finite_stability# RelStr st stability# R = 1 holds [#]R is Clique of R; registration :: I have done it through Ramsey. How else to prove it? :: For posets one gets it directly from Dilworth. :: Related: how big the gap between (clique# * stability#) and :: card of the carrier can be? cluster with_finite_clique# with_finite_stability# -> finite for RelStr; 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 :: DILWORTH:def 7 X \/ downarrow X; func Upper X -> Subset of R equals :: DILWORTH:def 8 X \/ uparrow X; end; theorem :: DILWORTH:22 :: 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; theorem :: DILWORTH:23 :: ABunion: for R being with_finite_stability# RelStr, A being StableSet of R st card A = stability# R holds Upper A \/ Lower A = [#]R; theorem :: DILWORTH:24 :: 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; theorem :: DILWORTH:25 :: 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; definition let R be RelStr; func minimals R -> Subset of R means :: DILWORTH:def 9 for x being Element of R holds x in it iff x is_minimal_in [#]R if R is non empty otherwise it = {}; func maximals R -> Subset of R means :: DILWORTH:def 10 for x being Element of R holds x in it iff x is_maximal_in [#]R if R is non empty otherwise it = {}; end; registration let R be with_finite_clique# non empty antisymmetric transitive RelStr; cluster maximals R -> non empty; cluster minimals R -> non empty; end; registration let R be RelStr; cluster minimals R -> stable; cluster maximals R -> stable; end; theorem :: DILWORTH:26 :: PCAamin: for R being RelStr, A being StableSet of R st not minimals R c= A holds not minimals R c= Upper A; theorem :: DILWORTH:27 :: PCAbmax: for R being RelStr, A being StableSet of R st not maximals R c= A holds not maximals R c= Lower A; begin :: Substructures registration let R be RelStr, X be finite Subset of R; cluster subrelstr X -> finite; end; theorem :: DILWORTH:28 :: SPClique: for R being RelStr, S being Subset of R, C being Clique of subrelstr S holds C is Clique of R; theorem :: DILWORTH:29 :: SPClique1: for R being RelStr, S being Subset of R, C being Clique of R holds C /\ S is Clique of subrelstr S; theorem :: DILWORTH:30 :: SPAChain1: for R being RelStr, S being Subset of R, A being StableSet of subrelstr S holds A is StableSet of R; theorem :: DILWORTH:31 :: SPAChain: for R being RelStr, S being Subset of R, A being StableSet of R holds A /\ S is StableSet of subrelstr S; theorem :: DILWORTH:32 :: 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; theorem :: DILWORTH:33 :: 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; theorem :: DILWORTH:34 :: 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; theorem :: DILWORTH:35 :: 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; registration let R be with_finite_clique# RelStr, S be Subset of R; cluster subrelstr S -> with_finite_clique#; end; registration let R be with_finite_stability# RelStr, S be Subset of R; cluster subrelstr S -> with_finite_stability#; end; theorem :: DILWORTH:36 :: 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); theorem :: DILWORTH:37 :: Pam: for R being with_finite_clique# antisymmetric transitive RelStr holds Upper minimals R = [#]R; theorem :: DILWORTH:38 :: 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); theorem :: DILWORTH:39 :: Pbm: for R being with_finite_clique# antisymmetric transitive RelStr holds Lower maximals R = [#]R; theorem :: DILWORTH:40 :: PCAmin: for R being with_finite_clique# antisymmetric transitive RelStr, A being StableSet of R st minimals R c= A holds A = minimals R; theorem :: DILWORTH:41 :: PCAmax: for R being with_finite_clique# antisymmetric transitive RelStr, A being StableSet of R st maximals R c= A holds A = maximals R; theorem :: DILWORTH:42 :: Hsubp0: for R being with_finite_clique# RelStr, S being Subset of R holds clique# subrelstr S <= clique# R; theorem :: DILWORTH:43 :: 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; theorem :: DILWORTH:44 :: Wsubp0: for R being with_finite_stability# RelStr, S being Subset of R holds stability# subrelstr S <= stability# R; theorem :: DILWORTH:45 :: 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; 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 :: DILWORTH:def 11 for x being set st x in P holds x is Clique of R; end; registration let R be RelStr; cluster Clique-wise for a_partition of the carrier of R; end; definition let R be RelStr; mode Clique-partition of R is Clique-wise a_partition of the carrier of R; end; registration let R be empty RelStr; cluster empty -> Clique-wise for a_partition of the carrier of R; end; theorem :: DILWORTH:46 :: Chpw: for R being finite RelStr, C being Clique-partition of R holds card C >= stability# R; theorem :: DILWORTH:47 :: 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; theorem :: DILWORTH:48 :: 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}; theorem :: DILWORTH:49 :: 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; definition let R be RelStr, P be a_partition of the carrier of R; attr P is StableSet-wise means :: DILWORTH:def 12 for x being set st x in P holds x is StableSet of R; end; registration let R be RelStr; cluster StableSet-wise for a_partition of the carrier of R; end; definition let R be RelStr; mode Coloring of R is StableSet-wise a_partition of the carrier of R; end; registration let R be empty RelStr; cluster -> StableSet-wise for a_partition of the carrier of R; end; theorem :: DILWORTH:50 :: ColClique: for R being finite RelStr, C being Coloring of R holds card C >= clique# R; begin :: Dilworth's theorem and a dual :: There seems to be little theory of antisymmetric transitive relations. :: Posets are required to be reflexive and antisymmetric while :: strict posets to be irreflexive and asymmetric (and both are :: required to be transitive.) Since asymmetric implies antisymmetric, :: it seems that the common ground would be antisymmetric and transitive :: relations. ::$N Dilworth's Decomposition Theorem theorem :: DILWORTH:51 :: Dilworth: Finite case for R being finite antisymmetric transitive RelStr ex C being Clique-partition of R st card(C) = stability# R; definition let R be with_finite_stability# non empty RelStr, C be Subset of R; attr C is strong-chain means :: DILWORTH:def 13 for S being finite non empty Subset of R ex P being Clique-partition of subrelstr S st card P <= stability# R & ex c being set st c in P & S /\ C c= c & for d being set st d in P & d <> c holds C /\ d = {}; end; registration let R be with_finite_stability# non empty RelStr; cluster strong-chain -> clique for Subset of R; end; registration let R be with_finite_stability# antisymmetric transitive non empty RelStr; cluster 1-element -> strong-chain for Subset of R; end; theorem :: DILWORTH:52 :: 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; theorem :: DILWORTH:53 :: Dilworth: General case for R being with_finite_stability# antisymmetric transitive RelStr ex C being Clique-partition of R st card C = stability# R; theorem :: DILWORTH:54 :: 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; begin :: Erdos-Szekeres theorem ::$N Erdos-Szekeres Theorem theorem :: DILWORTH:55 :: 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); :: 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 :: DILWORTH:56 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);