:: Dilworth's Decomposition Theorem for Posets
:: by Piotr Rudnicki
::
:: Copyright (c) 2009-2018 Association of Mizar Users

:: Facts that I could not find in MML.
scheme :: DILWORTH:sch 1
FraenkelFinCard1{ F1() -> non empty finite set , P1[ set ], F2() -> finite set , F3( set ) -> set } :
card F2() <= card F1()
provided
A1: F2() = { F3(w) where w is Element of F1() : P1[w] }
proof end;

theorem Th1: :: DILWORTH:1
for X, Y, x being set st not x in X holds
X \ (Y \/ {x}) = X \ Y
proof end;

theorem Th2: :: DILWORTH:2
for X, Y being set
for F being Subset-Family of X
for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)
proof end;

theorem Th3: :: DILWORTH:3
for X, Y being set
for F being a_partition of X
for G being a_partition of Y st X misses Y holds
F \/ G is a_partition of X \/ Y
proof end;

theorem Th4: :: DILWORTH:4
for X, Y being set
for F being a_partition of Y st Y c< X holds
F \/ {(X \ Y)} is a_partition of X
proof end;

theorem Th5: :: DILWORTH:5
for X being infinite set
for n being Nat ex Y being finite Subset of X st card Y > n
proof end;

definition
let R be RelStr ;
let S be Subset of R;
attr S is connected means :Def1: :: DILWORTH:def 1
the InternalRel of R is_connected_in S;
end;

:: deftheorem Def1 defines connected DILWORTH:def 1 :
for R being RelStr
for S being Subset of R holds
( S is connected iff the InternalRel of R is_connected_in S );

notation
let R be RelStr ;
let S be Subset of R;
synonym clique S for connected ;
end;

registration
let R be RelStr ;
cluster trivial -> clique for Subset of R;
coherence
for b1 being Subset of R st b1 is trivial holds
b1 is clique
proof end;
end;

registration
let R be RelStr ;
cluster clique for Subset of R;
existence
ex b1 being Subset of R st b1 is clique
proof end;
end;

definition
let R be RelStr ;
mode Clique of R is clique Subset of R;
end;

theorem Th6: :: DILWORTH:6
for R being RelStr
for S being Subset of R holds
( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a )
proof end;

registration
let R be RelStr ;
cluster finite connected for Clique of ;
existence
ex b1 being Clique of R st b1 is finite
proof end;
end;

registration
let R be reflexive RelStr ;
coherence
for b1 being Subset of R st b1 is connected holds
b1 is strongly_connected
proof end;
end;

registration
let R be non empty RelStr ;
cluster non empty finite connected for Clique of ;
existence
ex b1 being Clique of R st
( b1 is finite & not b1 is empty )
proof end;
end;

theorem :: DILWORTH:7
for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds
a2 <= a1
proof end;

theorem Th8: :: DILWORTH:8
for R being non empty RelStr
for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds
{a1,a2} is Clique of R
proof end;

theorem Th9: :: DILWORTH:9
for R being RelStr
for C being Clique of R
for S being Subset of C holds S is Clique of R
proof end;

theorem :: DILWORTH:10
for R being RelStr
for C being finite Clique of R
for n being Nat st n <= card C holds
ex B being finite Clique of R st
( B c= C & card B = n )
proof end;

theorem Th11: :: DILWORTH:11
for R being transitive RelStr
for C being Clique of R
for x, y being Element of R st x is_maximal_in C & x <= y holds
C \/ {y} is Clique of R
proof end;

theorem Th12: :: DILWORTH:12
for R being transitive RelStr
for C being Clique of R
for x, y being Element of R st x is_minimal_in C & y <= x holds
C \/ {y} is Clique of R
proof end;

definition
let R be RelStr ;
let S be Subset of R;
attr S is stable means :Def2: :: DILWORTH:def 2
for x, y being Element of R st x in S & y in S & x <> y holds
( not x <= y & not y <= x );
end;

:: deftheorem Def2 defines stable DILWORTH:def 2 :
for R being RelStr
for S being Subset of R holds
( S is stable iff for x, y being Element of R st x in S & y in S & x <> y holds
( not x <= y & not y <= x ) );

registration
let R be RelStr ;
cluster trivial -> stable for Subset of R;
coherence
for b1 being Subset of R st b1 is trivial holds
b1 is stable
by ZFMISC_1:def 10;
end;

registration
let R be RelStr ;
cluster stable for Subset of R;
existence
ex b1 being Subset of R st b1 is stable
proof end;
end;

definition
let R be RelStr ;
mode StableSet of R is stable Subset of R;
end;

registration
let R be RelStr ;
cluster finite stable for StableSet of ;
existence
ex b1 being StableSet of R st b1 is finite
proof end;
end;

registration
let R be non empty RelStr ;
cluster non empty finite stable for StableSet of ;
existence
ex b1 being StableSet of R st
( b1 is finite & not b1 is empty )
proof end;
end;

theorem :: DILWORTH:13
for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds
( not a1 <= a2 & not a2 <= a1 )
proof end;

theorem Th14: :: DILWORTH:14
for R being non empty RelStr
for a1, a2 being Element of R holds
( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )
proof end;

theorem Th15: :: DILWORTH:15
for R being RelStr
for C being Clique of R
for A being StableSet of R
for a, b being set st a in A & b in A & a in C & b in C holds
a = b
proof end;

theorem Th16: :: DILWORTH:16
for R being RelStr
for A being StableSet of R
for B being Subset of A holds B is StableSet of R
proof end;

theorem Th17: :: DILWORTH:17
for R being RelStr
for A being finite StableSet of R
for n being Nat st n <= card A holds
ex B being finite StableSet of R st card B = n
proof end;

definition
let R be RelStr ;
attr R is with_finite_clique# means :Def3: :: DILWORTH:def 3
ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C;
end;

:: deftheorem Def3 defines with_finite_clique# DILWORTH:def 3 :
for R being RelStr holds
( R is with_finite_clique# iff ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C );

registration
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_clique#
proof end;
end;

registration
let R be with_finite_clique# RelStr ;
cluster connected -> finite for Clique of ;
coherence
for b1 being Clique of R holds b1 is finite
proof end;
end;

definition
let R be with_finite_clique# RelStr ;
func clique# R -> Nat means :Def4: :: DILWORTH:def 4
( ex C being finite Clique of R st card C = it & ( for T being finite Clique of R holds card T <= it ) );
existence
ex b1 being Nat st
( ex C being finite Clique of R st card C = b1 & ( for T being finite Clique of R holds card T <= b1 ) )
proof end;
uniqueness
for b1, b2 being Nat st ex C being finite Clique of R st card C = b1 & ( for T being finite Clique of R holds card T <= b1 ) & ex C being finite Clique of R st card C = b2 & ( for T being finite Clique of R holds card T <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines clique# DILWORTH:def 4 :
for R being with_finite_clique# RelStr
for b2 being Nat holds
( b2 = clique# R iff ( ex C being finite Clique of R st card C = b2 & ( for T being finite Clique of R holds card T <= b2 ) ) );

registration
let R be empty RelStr ;
coherence
clique# R is empty
proof end;
end;

registration
let R be non empty with_finite_clique# RelStr ;
coherence
proof end;
end;

theorem :: DILWORTH:18
for R being non empty with_finite_clique# RelStr st [#] R is StableSet of R holds
clique# R = 1
proof end;

theorem Th19: :: DILWORTH:19
for R being with_finite_clique# RelStr st clique# R = 1 holds
[#] R is StableSet of R
proof end;

definition
let R be RelStr ;
attr R is with_finite_stability# means :Def5: :: DILWORTH:def 5
ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A;
end;

:: deftheorem Def5 defines with_finite_stability# DILWORTH:def 5 :
for R being RelStr holds
( R is with_finite_stability# iff ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A );

registration
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_stability#
proof end;
end;

registration
let R be with_finite_stability# RelStr ;
cluster stable -> finite for StableSet of ;
coherence
for b1 being StableSet of R holds b1 is finite
proof end;
end;

definition
let R be with_finite_stability# RelStr ;
func stability# R -> Nat means :Def6: :: DILWORTH:def 6
( ex A being finite StableSet of R st card A = it & ( for T being finite StableSet of R holds card T <= it ) );
existence
ex b1 being Nat st
( ex A being finite StableSet of R st card A = b1 & ( for T being finite StableSet of R holds card T <= b1 ) )
proof end;
uniqueness
for b1, b2 being Nat st ex A being finite StableSet of R st card A = b1 & ( for T being finite StableSet of R holds card T <= b1 ) & ex A being finite StableSet of R st card A = b2 & ( for T being finite StableSet of R holds card T <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines stability# DILWORTH:def 6 :
for R being with_finite_stability# RelStr
for b2 being Nat holds
( b2 = stability# R iff ( ex A being finite StableSet of R st card A = b2 & ( for T being finite StableSet of R holds card T <= b2 ) ) );

registration
let R be empty RelStr ;
coherence
proof end;
end;

registration
let R be non empty with_finite_stability# RelStr ;
coherence
proof end;
end;

theorem Th20: :: DILWORTH:20
for R being non empty with_finite_stability# RelStr st [#] R is Clique of R holds
stability# R = 1
proof end;

theorem Th21: :: DILWORTH:21
for R being with_finite_stability# RelStr st stability# R = 1 holds
[#] R is Clique of R
proof end;

registration
coherence
for b1 being RelStr st b1 is with_finite_clique# & b1 is with_finite_stability# holds
b1 is finite
proof end;
end;

definition
let R be RelStr ;
let X be Subset of R;
func Lower X -> Subset of R equals :: DILWORTH:def 7
X \/ ();
coherence
X \/ () is Subset of R
;
func Upper X -> Subset of R equals :: DILWORTH:def 8
X \/ ();
coherence
X \/ () is Subset of R
;
end;

:: deftheorem defines Lower DILWORTH:def 7 :
for R being RelStr
for X being Subset of R holds Lower X = X \/ ();

:: deftheorem defines Upper DILWORTH:def 8 :
for R being RelStr
for X being Subset of R holds Upper X = X \/ ();

theorem Th22: :: DILWORTH:22
for R being transitive antisymmetric RelStr
for A being StableSet of R
for z being set st z in Upper A & z in Lower A holds
z in A
proof end;

theorem Th23: :: DILWORTH:23
for R being with_finite_stability# RelStr
for A being StableSet of R st card A = stability# R holds
() \/ () = [#] R
proof end;

theorem Th24: :: DILWORTH:24
for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R
proof end;

theorem Th25: :: DILWORTH:25
for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R
proof end;

definition
let R be RelStr ;
set cR = the carrier of R;
func minimals R -> Subset of R means :Def9: :: DILWORTH:def 9
for x being Element of R holds
( x in it iff x is_minimal_in [#] R ) if not R is empty
otherwise it = {} ;
consistency
for b1 being Subset of R holds verum
;
existence
( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being Subset of R holds
( ( not R is empty & ( for x being Element of R holds
( x in b1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds
( x in b2 iff x is_minimal_in [#] R ) ) implies b1 = b2 ) & ( R is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
func maximals R -> Subset of R means :Def10: :: DILWORTH:def 10
for x being Element of R holds
( x in it iff x is_maximal_in [#] R ) if not R is empty
otherwise it = {} ;
consistency
for b1 being Subset of R holds verum
;
existence
( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_maximal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being Subset of R holds
( ( not R is empty & ( for x being Element of R holds
( x in b1 iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds
( x in b2 iff x is_maximal_in [#] R ) ) implies b1 = b2 ) & ( R is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
end;

:: deftheorem Def9 defines minimals DILWORTH:def 9 :
for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = minimals R iff for x being Element of R holds
( x in b2 iff x is_minimal_in [#] R ) ) ) & ( R is empty implies ( b2 = minimals R iff b2 = {} ) ) );

:: deftheorem Def10 defines maximals DILWORTH:def 10 :
for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = maximals R iff for x being Element of R holds
( x in b2 iff x is_maximal_in [#] R ) ) ) & ( R is empty implies ( b2 = maximals R iff b2 = {} ) ) );

registration
let R be non empty transitive antisymmetric with_finite_clique# RelStr ;
cluster maximals R -> non empty ;
coherence
not maximals R is empty
proof end;
cluster minimals R -> non empty ;
coherence
not minimals R is empty
proof end;
end;

registration
let R be RelStr ;
coherence
proof end;
coherence
proof end;
end;

theorem Th26: :: DILWORTH:26
for R being RelStr
for A being StableSet of R st not minimals R c= A holds
not minimals R c= Upper A
proof end;

theorem Th27: :: DILWORTH:27
for R being RelStr
for A being StableSet of R st not maximals R c= A holds
not maximals R c= Lower A
proof end;

registration
let R be RelStr ;
let X be finite Subset of R;
coherence by YELLOW_0:def 15;
end;

theorem Th28: :: DILWORTH:28
for R being RelStr
for S being Subset of R
for C being Clique of () holds C is Clique of R
proof end;

theorem Th29: :: DILWORTH:29
for R being RelStr
for S being Subset of R
for C being Clique of R holds C /\ S is Clique of ()
proof end;

theorem Th30: :: DILWORTH:30
for R being RelStr
for S being Subset of R
for A being StableSet of () holds A is StableSet of R
proof end;

theorem Th31: :: DILWORTH:31
for R being RelStr
for S being Subset of R
for A being StableSet of R holds A /\ S is StableSet of ()
proof end;

theorem Th32: :: DILWORTH:32
for R being RelStr
for S being Subset of R
for B being Subset of ()
for x being Element of ()
for y being Element of R st x = y & x is_maximal_in B holds
y is_maximal_in B
proof end;

theorem Th33: :: DILWORTH:33
for R being RelStr
for S being Subset of R
for B being Subset of ()
for x being Element of ()
for y being Element of R st x = y & x is_minimal_in B holds
y is_minimal_in B
proof end;

theorem Th34: :: DILWORTH:34
for R being transitive RelStr
for A being StableSet of R
for C being Clique of (subrelstr ())
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
proof end;

theorem Th35: :: DILWORTH:35
for R being transitive RelStr
for A being StableSet of R
for C being Clique of (subrelstr ())
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
proof end;

registration
let R be with_finite_clique# RelStr ;
let S be Subset of R;
coherence
proof end;
end;

registration
let R be with_finite_stability# RelStr ;
let S be Subset of R;
coherence
proof end;
end;

theorem Th36: :: DILWORTH:36
for R being non empty transitive antisymmetric with_finite_clique# RelStr
for x being Element of R ex y being Element of R st
( y is_minimal_in [#] R & ( y = x or y < x ) )
proof end;

theorem :: DILWORTH:37
for R being transitive antisymmetric with_finite_clique# RelStr holds Upper () = [#] R
proof end;

theorem Th38: :: DILWORTH:38
for R being non empty transitive antisymmetric with_finite_clique# RelStr
for x being Element of R ex y being Element of R st
( y is_maximal_in [#] R & ( y = x or x < y ) )
proof end;

theorem :: DILWORTH:39
for R being transitive antisymmetric with_finite_clique# RelStr holds Lower () = [#] R
proof end;

theorem Th40: :: DILWORTH:40
for R being transitive antisymmetric with_finite_clique# RelStr
for A being StableSet of R st minimals R c= A holds
A = minimals R
proof end;

theorem Th41: :: DILWORTH:41
for R being transitive antisymmetric with_finite_clique# RelStr
for A being StableSet of R st maximals R c= A holds
A = maximals R
proof end;

theorem Th42: :: DILWORTH:42
for R being with_finite_clique# RelStr
for S being Subset of R holds clique# () <= clique# R
proof end;

theorem :: DILWORTH:43
for R being with_finite_clique# RelStr
for C being Clique of R
for S being Subset of R st card C = clique# R & C c= S holds
clique# () = clique# R
proof end;

theorem Th44: :: DILWORTH:44
for R being with_finite_stability# RelStr
for S being Subset of R holds stability# () <= stability# R
proof end;

theorem Th45: :: DILWORTH:45
for R being with_finite_stability# RelStr
for A being StableSet of R
for S being Subset of R st card A = stability# R & A c= S holds
stability# () = stability# R
proof end;

definition
let R be RelStr ;
let P be a_partition of the carrier of R;
attr P is Clique-wise means :Def11: :: DILWORTH:def 11
for x being set st x in P holds
x is Clique of R;
end;

:: deftheorem Def11 defines Clique-wise DILWORTH:def 11 :
for R being RelStr
for P being a_partition of the carrier of R holds
( P is Clique-wise iff for x being set st x in P holds
x is Clique of R );

registration
let R be RelStr ;
cluster V40() with_non-empty_elements Clique-wise for a_partition of the carrier of R;
existence
ex b1 being a_partition of the carrier of R st b1 is Clique-wise
proof end;
end;

definition
let R be RelStr ;
mode Clique-partition of R is Clique-wise a_partition of the carrier of R;
end;

registration
let R be empty RelStr ;
cluster empty -> Clique-wise for a_partition of the carrier of R;
coherence
for b1 being a_partition of the carrier of R st b1 is empty holds
b1 is Clique-wise
;
end;

theorem Th46: :: DILWORTH:46
for R being finite RelStr
for C being Clique-partition of R holds card C >= stability# R
proof end;

theorem Th47: :: DILWORTH:47
for R being with_finite_stability# RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )
proof end;

theorem Th48: :: DILWORTH:48
for R being finite RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
proof end;

theorem Th49: :: DILWORTH:49
for R being non empty transitive antisymmetric with_finite_stability# RelStr
for A being StableSet of R
for U being Clique-partition of (subrelstr ())
for L being Clique-partition of (subrelstr ()) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
proof end;

definition
let R be RelStr ;
let P be a_partition of the carrier of R;
attr P is StableSet-wise means :Def12: :: DILWORTH:def 12
for x being set st x in P holds
x is StableSet of R;
end;

:: deftheorem Def12 defines StableSet-wise DILWORTH:def 12 :
for R being RelStr
for P being a_partition of the carrier of R holds
( P is StableSet-wise iff for x being set st x in P holds
x is StableSet of R );

registration
let R be RelStr ;
existence
ex b1 being a_partition of the carrier of R st b1 is StableSet-wise
proof end;
end;

definition
let R be RelStr ;
mode Coloring of R is StableSet-wise a_partition of the carrier of R;
end;

registration
let R be empty RelStr ;
cluster -> StableSet-wise for a_partition of the carrier of R;
coherence
for b1 being a_partition of the carrier of R holds b1 is StableSet-wise
;
end;

theorem :: DILWORTH:50
for R being finite RelStr
for C being Coloring of R holds card C >= clique# R
proof end;

:: 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.
:: Dilworth's Decomposition Theorem
theorem Th51: :: DILWORTH:51
for R being finite transitive antisymmetric RelStr ex C being Clique-partition of R st card C = stability# R
proof end;

definition
let R be non empty with_finite_stability# RelStr ;
let C be Subset of R;
attr C is strong-chain means :: DILWORTH:def 13
for S being non empty finite Subset of R ex P being Clique-partition of () st
( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) );
end;

:: deftheorem defines strong-chain DILWORTH:def 13 :
for R being non empty with_finite_stability# RelStr
for C being Subset of R holds
( C is strong-chain iff for S being non empty finite Subset of R ex P being Clique-partition of () st
( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) ) );

registration
let R be non empty with_finite_stability# RelStr ;
cluster strong-chain -> clique for Subset of R;
coherence
for b1 being Subset of R st b1 is strong-chain holds
b1 is clique
proof end;
end;

registration
let R be non empty transitive antisymmetric with_finite_stability# RelStr ;
cluster 1 -element -> strong-chain for Subset of R;
coherence
for b1 being Subset of R st b1 is 1 -element holds
b1 is strong-chain
proof end;
end;

theorem Th52: :: DILWORTH:52
for R being non empty transitive antisymmetric with_finite_stability# RelStr ex S being non empty Subset of R st
( S is strong-chain & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
proof end;

theorem :: DILWORTH:53
for R being transitive antisymmetric with_finite_stability# RelStr ex C being Clique-partition of R st card C = stability# R
proof end;

theorem :: DILWORTH:54
for R being transitive antisymmetric with_finite_clique# RelStr ex A being Coloring of R st card A = clique# R
proof end;

:: Erdos-Szekeres Theorem
theorem Th55: :: DILWORTH:55
for R being finite transitive antisymmetric RelStr
for r, s being Nat holds
( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )
proof 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 :: DILWORTH:56
for f being real-valued FinSequence
for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds
ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )
proof end;