:: Dilworth's Decomposition Theorem for Posets
:: by Piotr Rudnicki
::
:: Received September 17, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem set00: :: DILWORTH:1
for
X,
Y,
x being
set st not
x in X holds
X \ (Y \/ {x}) = X \ Y
theorem ssf0: :: DILWORTH:2
theorem SPpart0: :: DILWORTH:3
theorem SPpart: :: DILWORTH:4
theorem Sinfset: :: DILWORTH:5
:: deftheorem Lclique defines connected DILWORTH:def 1 :
theorem DClique: :: DILWORTH:6
theorem :: DILWORTH:7
theorem Clique36b: :: DILWORTH:8
theorem Clique37: :: DILWORTH:9
theorem :: DILWORTH:10
theorem ExtClique: :: DILWORTH:11
theorem ExtCliquemin: :: DILWORTH:12
:: deftheorem LAChain defines stable DILWORTH:def 2 :
theorem :: DILWORTH:13
theorem AChain36b: :: DILWORTH:14
theorem ACClique: :: DILWORTH:15
theorem AChain0: :: DILWORTH:16
theorem AChain1: :: DILWORTH:17
:: deftheorem Lfheight defines with_finite_clique# DILWORTH:def 3 :
:: deftheorem Lheight defines clique# DILWORTH:def 4 :
theorem :: DILWORTH:18
theorem Height4: :: DILWORTH:19
:: deftheorem Lfwidth defines with_finite_stability# DILWORTH:def 5 :
:: deftheorem Lwidth defines stability# DILWORTH:def 6 :
theorem Width3: :: DILWORTH:20
theorem Width4: :: DILWORTH:21
:: deftheorem defines Lower DILWORTH:def 7 :
:: deftheorem defines Upper DILWORTH:def 8 :
theorem ABAC0: :: DILWORTH:22
theorem ABunion: :: DILWORTH:23
theorem Pminmin: :: DILWORTH:24
theorem Pmaxmax: :: DILWORTH:25
:: deftheorem Lmin defines minimals DILWORTH:def 9 :
:: deftheorem Lmax defines maximals DILWORTH:def 10 :
theorem PCAamin: :: DILWORTH:26
theorem PCAbmax: :: DILWORTH:27
theorem SPClique: :: DILWORTH:28
theorem SPClique1: :: DILWORTH:29
theorem SPAChain1: :: DILWORTH:30
theorem SPAChain: :: DILWORTH:31
theorem SPmax: :: DILWORTH:32
theorem SPmin: :: DILWORTH:33
theorem PbeSmax: :: DILWORTH:34
theorem PabSmin: :: DILWORTH:35
theorem Pmaxmin: :: DILWORTH:36
theorem :: DILWORTH:37
theorem Pminmax: :: DILWORTH:38
theorem :: DILWORTH:39
theorem PCAmin: :: DILWORTH:40
theorem PCAmax: :: DILWORTH:41
theorem Hsubp0: :: DILWORTH:42
theorem :: DILWORTH:43
theorem Wsubp0: :: DILWORTH:44
theorem Wsubp1: :: DILWORTH:45
:: deftheorem LCpart defines Clique-wise DILWORTH:def 11 :
theorem Chpw: :: DILWORTH:46
theorem ACpart1: :: DILWORTH:47
theorem ACpart2: :: DILWORTH:48
theorem Main: :: DILWORTH:49
:: deftheorem LACpart defines StableSet-wise DILWORTH:def 12 :
theorem :: DILWORTH:50
theorem DWf: :: DILWORTH:51
:: deftheorem Lsc defines strong-chain DILWORTH:def 13 :
theorem Maxsc: :: DILWORTH:52
theorem :: DILWORTH:53
theorem :: DILWORTH:54
theorem CSR: :: DILWORTH:55
theorem :: DILWORTH:56