begin
theorem set00:
for
X,
Y,
x being
set st not
x in X holds
X \ (Y \/ {x}) = X \ Y
theorem ssf0:
theorem SPpart0:
theorem SPpart:
theorem Sinfset:
begin
:: deftheorem Lclique 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 );
theorem DClique:
theorem
theorem Clique36b:
theorem Clique37:
theorem
theorem ExtClique:
theorem ExtCliquemin:
:: deftheorem LAChain 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 ) );
theorem
theorem AChain36b:
theorem ACClique:
theorem AChain0:
theorem AChain1:
begin
:: deftheorem Lfheight 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 );
:: deftheorem Lheight 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 ) ) );
theorem
theorem Height4:
:: deftheorem Lfwidth 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 );
:: deftheorem Lwidth 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 ) ) );
theorem Width3:
theorem Width4:
begin
:: deftheorem defines Lower DILWORTH:def 7 :
for R being RelStr
for X being Subset of R holds Lower X = X \/ (downarrow X);
:: deftheorem defines Upper DILWORTH:def 8 :
for R being RelStr
for X being Subset of R holds Upper X = X \/ (uparrow X);
theorem ABAC0:
theorem ABunion:
theorem Pminmin:
theorem Pmaxmax:
:: deftheorem Lmin 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 Lmax 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 = {} ) ) );
theorem PCAamin:
theorem PCAbmax:
begin
theorem SPClique:
theorem SPClique1:
theorem SPAChain1:
theorem SPAChain:
theorem SPmax:
theorem SPmin:
theorem PbeSmax:
theorem PabSmin:
theorem Pmaxmin:
theorem
theorem Pminmax:
theorem
theorem PCAmin:
theorem PCAmax:
theorem Hsubp0:
theorem
theorem Wsubp0:
theorem Wsubp1:
begin
:: deftheorem LCpart 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 );
theorem Chpw:
theorem ACpart1:
theorem ACpart2:
theorem Main:
:: deftheorem LACpart 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 );
theorem
begin
theorem DWf:
:: deftheorem Lsc 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 (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 = {} ) ) ) );
theorem Maxsc:
theorem
theorem
begin
theorem CSR:
theorem