:: Dilworth's Decomposition Theorem for Posets :: by Piotr Rudnicki :: :: Received September 17, 2009 :: Copyright (c) 2009-2015 Association of Mizar Users
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 )
:: 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
:: 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