### The Mizar article:

### Completely-Irreducible Elements

**by****Robert Milewski**

- Received February 9, 1998
Copyright (c) 1998 Association of Mizar Users

- MML identifier: WAYBEL16
- [ MML identifier index ]

environ vocabulary WAYBEL_0, LATTICES, BOOLE, ORDERS_1, ORDERS_2, LATTICE3, OPPCAT_1, RELAT_1, RELAT_2, FILTER_0, QUANTAL1, FILTER_2, BHSP_3, PRE_TOPC, FUNCOP_1, FUNCT_1, YELLOW_0, SEQM_3, FINSET_1, ORDINAL2, YELLOW_1, SETFAM_1, WELLORD2, TARSKI, WAYBEL_1, WAYBEL_6, WAYBEL_2, SUBSET_1, WAYBEL_3, WAYBEL_8, COMPTS_1, WAYBEL16; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1, FINSET_1, FUNCT_2, FUNCOP_1, ORDERS_1, PRE_TOPC, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_4, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_8; constructors ORDERS_3, YELLOW_4, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_4, WAYBEL_8, MEMBERED; clusters STRUCT_0, FINSET_1, LATTICE3, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_8, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1; requirements BOOLE, SUBSET; definitions TARSKI, XBOOLE_0; theorems TARSKI, SUBSET_1, SETFAM_1, RELAT_1, ZFMISC_1, FINSET_1, FUNCOP_1, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_7, WAYBEL_8, WAYBEL13, WAYBEL14, WAYBEL15, XBOOLE_0, XBOOLE_1; schemes YELLOW_2, WAYBEL_3; begin :: Preliminaries theorem Th1: for L be sup-Semilattice for x,y be Element of L holds "/\"((uparrow x) /\ (uparrow y),L) = x "\/" y proof let L be sup-Semilattice; let x,y be Element of L; (uparrow x) /\ (uparrow y) = uparrow (x "\/" y) by WAYBEL14:4; hence "/\"((uparrow x) /\ (uparrow y),L) = x "\/" y by WAYBEL_0:39; end; theorem for L be Semilattice for x,y be Element of L holds "\/"((downarrow x) /\ (downarrow y),L) = x "/\" y proof let L be Semilattice; let x,y be Element of L; (downarrow x) /\ (downarrow y) = downarrow (x "/\" y) by WAYBEL14:3; hence "\/"((downarrow x) /\ (downarrow y),L) = x "/\" y by WAYBEL_0:34; end; theorem Th3: for L be non empty RelStr for x,y be Element of L st x is_maximal_in (the carrier of L) \ uparrow y holds (uparrow x) \ {x} = (uparrow x) /\ (uparrow y) proof let L be non empty RelStr; let x,y be Element of L; assume A1: x is_maximal_in (the carrier of L) \ uparrow y; then x in (the carrier of L) \ uparrow y by WAYBEL_4:56; then not x in uparrow y by XBOOLE_0:def 4; then A2: not y <= x by WAYBEL_0:18; thus (uparrow x) \ {x} c= (uparrow x) /\ (uparrow y) proof let a be set; assume A3: a in (uparrow x) \ {x}; then A4: a in uparrow x & not a in {x} by XBOOLE_0:def 4; reconsider a1 = a as Element of L by A3; x <= a1 & a1 <> x by A4,TARSKI:def 1,WAYBEL_0:18; then x < a1 by ORDERS_1:def 10; then not a1 in (the carrier of L) \ uparrow y by A1,WAYBEL_4:56; then a in uparrow y by XBOOLE_0:def 4; hence a in (uparrow x) /\ (uparrow y) by A4,XBOOLE_0:def 3; end; let a be set; assume A5: a in (uparrow x) /\ (uparrow y); then A6: a in uparrow x & a in uparrow y by XBOOLE_0:def 3; reconsider a1 = a as Element of L by A5; y <= a1 by A6,WAYBEL_0:18; then not a in {x} by A2,TARSKI:def 1; hence a in (uparrow x) \ {x} by A6,XBOOLE_0:def 4; end; theorem for L be non empty RelStr for x,y be Element of L st x is_minimal_in (the carrier of L) \ downarrow y holds (downarrow x) \ {x} = (downarrow x) /\ (downarrow y) proof let L be non empty RelStr; let x,y be Element of L; assume A1: x is_minimal_in (the carrier of L) \ downarrow y; then x in (the carrier of L) \ downarrow y by WAYBEL_4:57; then not x in downarrow y by XBOOLE_0:def 4; then A2: not x <= y by WAYBEL_0:17; thus (downarrow x) \ {x} c= (downarrow x) /\ (downarrow y) proof let a be set; assume A3: a in (downarrow x) \ {x}; then A4: a in downarrow x & not a in {x} by XBOOLE_0:def 4; reconsider a1 = a as Element of L by A3; a1 <= x & a1 <> x by A4,TARSKI:def 1,WAYBEL_0:17; then a1 < x by ORDERS_1:def 10; then not a1 in (the carrier of L) \ downarrow y by A1,WAYBEL_4:57; then a in downarrow y by XBOOLE_0:def 4; hence a in (downarrow x) /\ (downarrow y) by A4,XBOOLE_0:def 3; end; let a be set; assume A5: a in (downarrow x) /\ (downarrow y); then A6: a in downarrow x & a in downarrow y by XBOOLE_0:def 3; reconsider a1 = a as Element of L by A5; a1 <= y by A6,WAYBEL_0:17; then not a in {x} by A2,TARSKI:def 1; hence a in (downarrow x) \ {x} by A6,XBOOLE_0:def 4; end; theorem Th5: for L be with_suprema Poset for X,Y be Subset of L for X',Y' be Subset of L opp st X = X' & Y = Y' holds X "\/" Y = X' "/\" Y' proof let L be with_suprema Poset; let X,Y be Subset of L; let X',Y' be Subset of L opp; assume that A1: X = X' and A2: Y = Y'; thus X "\/" Y c= X' "/\" Y' proof let a be set; assume a in X "\/" Y; then a in { p "\/" q where p,q is Element of L : p in X & q in Y } by YELLOW_4:def 3; then consider x,y be Element of L such that A3: a = x "\/" y and A4: x in X and A5: y in Y; A6: x~ in X' & y~ in Y' by A1,A2,A4,A5,LATTICE3:def 6; a = x~ "/\" y~ by A3,YELLOW_7:23; then a in { p "/\" q where p,q is Element of L opp : p in X' & q in Y' } by A6; hence a in X' "/\" Y' by YELLOW_4:def 4; end; let a be set; assume a in X' "/\" Y'; then a in { p "/\" q where p,q is Element of L opp : p in X' & q in Y' } by YELLOW_4:def 4; then consider x,y be Element of L opp such that A7: a = x "/\" y and A8: x in X' and A9: y in Y'; A10: ~x in X & ~y in Y by A1,A2,A8,A9,LATTICE3:def 7; a = ~x "\/" ~y by A7,YELLOW_7:24; then a in { p "\/" q where p,q is Element of L : p in X & q in Y } by A10; hence a in X "\/" Y by YELLOW_4:def 3; end; theorem for L be with_infima Poset for X,Y be Subset of L for X',Y' be Subset of L opp st X = X' & Y = Y' holds X "/\" Y = X' "\/" Y' proof let L be with_infima Poset; let X,Y be Subset of L; let X',Y' be Subset of L opp; assume that A1: X = X' and A2: Y = Y'; thus X "/\" Y c= X' "\/" Y' proof let a be set; assume a in X "/\" Y; then a in { p "/\" q where p,q is Element of L : p in X & q in Y } by YELLOW_4:def 4; then consider x,y be Element of L such that A3: a = x "/\" y and A4: x in X and A5: y in Y; A6: x~ in X' & y~ in Y' by A1,A2,A4,A5,LATTICE3:def 6; a = x~ "\/" y~ by A3,YELLOW_7:21; then a in { p "\/" q where p,q is Element of L opp : p in X' & q in Y' } by A6; hence a in X' "\/" Y' by YELLOW_4:def 3; end; let a be set; assume a in X' "\/" Y'; then a in { p "\/" q where p,q is Element of L opp : p in X' & q in Y' } by YELLOW_4:def 3; then consider x,y be Element of L opp such that A7: a = x "\/" y and A8: x in X' and A9: y in Y'; A10: ~x in X & ~y in Y by A1,A2,A8,A9,LATTICE3:def 7; a = ~x "/\" ~y by A7,YELLOW_7:22; then a in { p "/\" q where p,q is Element of L : p in X & q in Y } by A10; hence a in X "/\" Y by YELLOW_4:def 4; end; theorem Th7: for L be non empty reflexive transitive RelStr holds Filt L = Ids (L opp) proof let L be non empty reflexive transitive RelStr; A1: Filt L c= Ids (L opp) proof let x be set; assume x in Filt L; then x in { X where X is Filter of L : not contradiction } by WAYBEL_0:def 24; then consider x1 be Filter of L such that A2: x1 = x; A3: x1 is lower Subset of L opp by YELLOW_7:29; x1 is directed Subset of L opp by YELLOW_7:27; then x in { X where X is Ideal of L opp : not contradiction } by A2,A3; hence x in Ids (L opp) by WAYBEL_0:def 23; end; Ids (L opp) c= Filt L proof let x be set; assume x in Ids L opp; then x in { X where X is Ideal of L opp : not contradiction } by WAYBEL_0:def 23; then consider x1 be Ideal of L opp such that A4: x1 = x; A5: x1 is upper Subset of L by YELLOW_7:29; x1 is filtered Subset of L by YELLOW_7:27; then x in { X where X is Filter of L : not contradiction } by A4,A5; hence x in Filt L by WAYBEL_0:def 24; end; hence Filt L = Ids (L opp) by A1,XBOOLE_0:def 10; end; theorem for L be non empty reflexive transitive RelStr holds Ids L = Filt (L opp) proof let L be non empty reflexive transitive RelStr; A1: Ids L c= Filt (L opp) proof let x be set; assume x in Ids L; then x in { X where X is Ideal of L : not contradiction } by WAYBEL_0:def 23; then consider x1 be Ideal of L such that A2: x1 = x; A3: x1 is upper Subset of L opp by YELLOW_7:28; x1 is filtered Subset of L opp by YELLOW_7:26; then x in { X where X is Filter of L opp : not contradiction } by A2,A3; hence x in Filt (L opp) by WAYBEL_0:def 24; end; Filt (L opp) c= Ids L proof let x be set; assume x in Filt L opp; then x in { X where X is Filter of L opp : not contradiction } by WAYBEL_0:def 24; then consider x1 be Filter of L opp such that A4: x1 = x; A5: x1 is lower Subset of L by YELLOW_7:28; x1 is directed Subset of L by YELLOW_7:26; then x in { X where X is Ideal of L : not contradiction } by A4,A5; hence x in Ids L by WAYBEL_0:def 23; end; hence Ids L = Filt (L opp) by A1,XBOOLE_0:def 10; end; begin :: Free Generation Set definition let S,T be complete (non empty Poset); mode CLHomomorphism of S,T -> map of S,T means it is directed-sups-preserving infs-preserving; existence proof reconsider f = (the carrier of S) --> Top T as Function of the carrier of S,the carrier of T by FUNCOP_1:58; reconsider f as map of S,T; take f; now let X be Subset of S; assume A1: X is non empty directed; now assume ex_sup_of X,S; now let x,y be Element of S; assume x <= y; f.x = Top T by FUNCOP_1:13 .= f.y by FUNCOP_1:13; hence f.x <= f.y; end; then A2: f is monotone by WAYBEL_1:def 2; rng f = {Top T} by FUNCOP_1:14; then A3: f.:X c= {Top T} by RELAT_1:144; for X be non empty Subset of S holds f.:X is non empty; then A4: f.:X is non empty finite directed Subset of T by A1,A2,A3,FINSET_1:13,YELLOW_2:17; then sup (f.:X) in f.:X by WAYBEL_3:16; then A5: sup (f.:X) = Top T by A3,TARSKI:def 1; thus ex_sup_of f.:X,T by A4,WAYBEL_0:75; thus sup (f.:X) = f.sup X by A5,FUNCOP_1:13; end; hence f preserves_sup_of X by WAYBEL_0:def 31; end; hence f is directed-sups-preserving by WAYBEL_0:def 37; now let X be Subset of S; now assume ex_inf_of X,S; rng f = {Top T} by FUNCOP_1:14; then A6: f.:X is Subset of {Top T} by RELAT_1:144; thus ex_inf_of f.:X,T by YELLOW_0:17; now per cases; suppose f.:X = {}; hence inf (f.:X) = Top T by YELLOW_0:def 12 .= f.inf X by FUNCOP_1:13; suppose f.:X <> {}; then f.:X = {Top T} by A6,ZFMISC_1:39; hence inf (f.:X) = Top T by YELLOW_0:39 .= f.inf X by FUNCOP_1:13; end; hence inf (f.:X) = f.inf X; end; hence f preserves_inf_of X by WAYBEL_0:def 30; end; hence f is infs-preserving by WAYBEL_0:def 32; end; end; definition let S be continuous complete (non empty Poset); let A be Subset of S; pred A is_FG_set means for T be continuous complete (non empty Poset) for f be Function of A,the carrier of T ex h be CLHomomorphism of S,T st h|A = f & for h' be CLHomomorphism of S,T st h'|A = f holds h' = h; end; definition let L be upper-bounded non empty Poset; cluster Filt L -> non empty; coherence proof now let x,y be Element of L; assume that A1: x in {Top L} and A2: x <= y; x = Top L by A1,TARSKI:def 1; then y = Top L by A2,WAYBEL15:5; hence y in {Top L} by TARSKI:def 1; end; then {Top L} is Filter of L by WAYBEL_0:5,def 20; then {Top L} in {Y where Y is Filter of L : not contradiction}; hence thesis by WAYBEL_0:def 24; end; end; theorem Th9: for X be set for Y be non empty Subset of InclPoset Filt BoolePoset X holds meet Y is Filter of BoolePoset X proof let X be set; set L = BoolePoset X; let Y be non empty Subset of InclPoset Filt L; A1: now let Z be set; assume Z in Y; then Z in the carrier of InclPoset Filt L; then Z in the carrier of RelStr(#Filt L, RelIncl (Filt L)#) by YELLOW_1:def 1; then Z in { V where V is Filter of L : not contradiction } by WAYBEL_0:def 24; then consider Z1 be Filter of L such that A2: Z1 = Z; thus Top L in Z by A2,WAYBEL_4:22; end; Y c= the carrier of InclPoset Filt L; then A3: Y c= the carrier of RelStr(#Filt L, RelIncl (Filt L)#) by YELLOW_1:def 1; A4: Y c= bool the carrier of L proof let v be set; assume v in Y; then v in Filt L by A3; then v in { V where V is Filter of L : not contradiction } by WAYBEL_0:def 24; then consider v1 be Filter of L such that A5: v1 = v; thus v in bool the carrier of L by A5; end; A6: for Z be Subset of L st Z in Y holds Z is upper proof let Z be Subset of L; assume Z in Y; then Z in Filt L by A3; then Z in { V where V is Filter of L : not contradiction } by WAYBEL_0:def 24; then consider Z1 be Filter of L such that A7: Z1 = Z; thus Z is upper by A7; end; now let V be Subset of L; assume V in Y; then V in Filt L by A3; then V in { Z where Z is Filter of L : not contradiction } by WAYBEL_0:def 24; then consider V1 be Filter of L such that A8: V1 = V; thus V is upper by A8; thus V is filtered by A8; end; hence meet Y is Filter of L by A1,A4,A6,SETFAM_1:def 1,YELLOW_2:39,41; end; theorem for X be set for Y be non empty Subset of InclPoset Filt BoolePoset X holds ex_inf_of Y,InclPoset Filt BoolePoset X & "/\"(Y,InclPoset Filt BoolePoset X) = meet Y proof let X be set; set L = InclPoset Filt BoolePoset X; let Y be non empty Subset of L; meet Y is Filter of BoolePoset X by Th9; then meet Y in { Z where Z is Filter of BoolePoset X: not contradiction }; then meet Y in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by WAYBEL_0:def 24; then meet Y in the carrier of L by YELLOW_1:def 1; then reconsider a = meet Y as Element of L; now let b be Element of L; assume b in Y; then meet Y c= b by SETFAM_1:4; hence a <= b by YELLOW_1:3; end; then A1: a is_<=_than Y by LATTICE3:def 8; for b be Element of L st b is_<=_than Y holds b <= a proof let b be Element of L; assume A2: b is_<=_than Y; now let x be set; assume A3: x in Y; then reconsider x' = x as Element of L; b <= x' by A2,A3,LATTICE3:def 8; hence b c= x by YELLOW_1:3; end; then b c= meet Y by SETFAM_1:6; hence b <= a by YELLOW_1:3; end; hence ex_inf_of Y,InclPoset Filt BoolePoset X & "/\"(Y,InclPoset Filt BoolePoset X) = meet Y by A1,YELLOW_0:31; end; theorem Th11: for X be set holds bool X is Filter of BoolePoset X proof let X be set; bool X c= the carrier of BoolePoset X by WAYBEL_7:4; then reconsider A = bool X as non empty Subset of BoolePoset X ; for x,y be set st x c= y & y c= X & x in A holds y in A; then A1: A is upper by WAYBEL_7:11; now let x,y be set; assume that A2: x in A and A3: y in A; x /\ y c= X /\ X by A2,A3,XBOOLE_1:27; hence x /\ y in A; end; hence bool X is Filter of BoolePoset X by A1,WAYBEL_7:13; end; theorem Th12: for X be set holds {X} is Filter of BoolePoset X proof let X be set; now let c be set; assume c in {X}; then c = X by TARSKI:def 1; then c is Element of BoolePoset X by WAYBEL_8:28; hence c in the carrier of BoolePoset X; end; then {X} c= the carrier of BoolePoset X by TARSKI:def 3; then reconsider A = {X} as non empty Subset of BoolePoset X ; for x,y be set st x c= y & y c= X & x in A holds y in A proof let x,y be set; assume that A1: x c= y and A2: y c= X and A3: x in A; x = X by A3,TARSKI:def 1; then y = X by A1,A2,XBOOLE_0:def 10; hence y in A by TARSKI:def 1; end; then A4: A is upper by WAYBEL_7:11; now let x,y be set; assume that A5: x in A and A6: y in A; x = X & y = X by A5,A6,TARSKI:def 1; hence x /\ y in A by TARSKI:def 1; end; hence thesis by A4,WAYBEL_7:13; end; theorem for X be set holds InclPoset Filt BoolePoset X is upper-bounded proof let X be set; set L = InclPoset Filt BoolePoset X; bool X is Filter of BoolePoset X by Th11; then bool X in { Z where Z is Filter of BoolePoset X: not contradiction }; then bool X in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by WAYBEL_0:def 24; then bool X in the carrier of L by YELLOW_1:def 1; then reconsider x = bool X as Element of L; now let b be Element of L; assume b in the carrier of L; then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by YELLOW_1:def 1; then b in { V where V is Filter of BoolePoset X : not contradiction } by WAYBEL_0:def 24; then consider b1 be Filter of BoolePoset X such that A1: b1 = b; b c= the carrier of BoolePoset X by A1; then b c= bool X by WAYBEL_7:4; hence b <= x by YELLOW_1:3; end; then x is_>=_than the carrier of L by LATTICE3:def 9; hence L is upper-bounded by YELLOW_0:def 5; end; theorem for X be set holds InclPoset Filt BoolePoset X is lower-bounded proof let X be set; set L = InclPoset Filt BoolePoset X; {X} is Filter of BoolePoset X by Th12; then {X} in { Z where Z is Filter of BoolePoset X: not contradiction }; then {X} in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by WAYBEL_0:def 24; then {X} in the carrier of L by YELLOW_1:def 1; then reconsider x = {X} as Element of L; now let b be Element of L; assume b in the carrier of L; then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by YELLOW_1:def 1; then b in { V where V is Filter of BoolePoset X : not contradiction } by WAYBEL_0:def 24; then consider b1 be Filter of BoolePoset X such that A1: b1 = b; consider d be set such that A2: d in b1 by XBOOLE_0:def 1; d is Element of BoolePoset X by A2; then A3: d c= X by WAYBEL_8:28; now let c be set; assume c in {X}; then c = X by TARSKI:def 1; hence c in b by A1,A2,A3,WAYBEL_7:11; end; then {X} c= b by TARSKI:def 3; hence x <= b by YELLOW_1:3; end; then x is_<=_than the carrier of L by LATTICE3:def 8; hence L is lower-bounded by YELLOW_0:def 4; end; theorem for X be set holds Top (InclPoset Filt BoolePoset X) = bool X proof let X be set; set L = InclPoset Filt BoolePoset X; bool X is Filter of BoolePoset X by Th11; then bool X in { Z where Z is Filter of BoolePoset X: not contradiction }; then bool X in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by WAYBEL_0:def 24; then bool X in the carrier of L by YELLOW_1:def 1; then reconsider bX = bool X as Element of L; A1: bX is_<=_than {} by YELLOW_0:6; for b be Element of L st b is_<=_than {} holds bX >= b proof let b be Element of L; assume b is_<=_than {}; b in the carrier of L; then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by YELLOW_1:def 1; then b in { V where V is Filter of BoolePoset X : not contradiction } by WAYBEL_0:def 24; then consider b1 be Filter of BoolePoset X such that A2: b1 = b; b c= the carrier of BoolePoset X by A2; then b c= bool X by WAYBEL_7:4; hence bX >= b by YELLOW_1:3; end; then "/\"({},L) = bool X by A1,YELLOW_0:31; hence Top (InclPoset Filt BoolePoset X) = bool X by YELLOW_0:def 12; end; theorem for X be set holds Bottom (InclPoset Filt BoolePoset X) = {X} proof let X be set; set L = InclPoset Filt BoolePoset X; {X} is Filter of BoolePoset X by Th12; then {X} in { Z where Z is Filter of BoolePoset X: not contradiction }; then {X} in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by WAYBEL_0:def 24; then {X} in the carrier of L by YELLOW_1:def 1; then reconsider bX = {X} as Element of L; A1: bX is_>=_than {} by YELLOW_0:6; for b be Element of L st b is_>=_than {} holds bX <= b proof let b be Element of L; assume b is_>=_than {}; b in the carrier of L; then b in the carrier of RelStr(#Filt BoolePoset X, RelIncl (Filt BoolePoset X)#) by YELLOW_1:def 1; then b in { V where V is Filter of BoolePoset X : not contradiction } by WAYBEL_0:def 24; then consider b1 be Filter of BoolePoset X such that A2: b1 = b; consider d be set such that A3: d in b1 by XBOOLE_0:def 1; d is Element of BoolePoset X by A3; then A4: d c= X by WAYBEL_8:28; now let c be set; assume c in {X}; then c = X by TARSKI:def 1; hence c in b by A2,A3,A4,WAYBEL_7:11; end; then {X} c= b by TARSKI:def 3; hence bX <= b by YELLOW_1:3; end; then "\/"({},L) = {X} by A1,YELLOW_0:30; hence Bottom (InclPoset Filt BoolePoset X) = {X} by YELLOW_0:def 11; end; theorem for X be non empty set for Y be non empty Subset of InclPoset X st ex_sup_of Y,InclPoset X holds union Y c= sup Y proof let X be non empty set; let Y be non empty Subset of InclPoset X; assume A1: ex_sup_of Y,InclPoset X; now let x be set; assume A2: x in Y; then reconsider x1 = x as Element of InclPoset X; sup Y is_>=_than Y by A1,YELLOW_0:30; then sup Y >= x1 by A2,LATTICE3:def 9; hence x c= sup Y by YELLOW_1:3; end; hence union Y c= sup Y by ZFMISC_1:94; end; theorem Th18: for L be upper-bounded Semilattice holds InclPoset Filt L is complete proof let L be upper-bounded Semilattice; InclPoset Ids (L opp) is complete; hence InclPoset Filt L is complete by Th7; end; definition let L be upper-bounded Semilattice; cluster InclPoset Filt L -> complete; coherence by Th18; end; begin :: Completely-irreducible Elements definition :: DEFINITION 4.19 let L be non empty RelStr; let p be Element of L; attr p is completely-irreducible means :Def3: ex_min_of (uparrow p)\{p},L; end; theorem Th19: for L be non empty RelStr for p be Element of L st p is completely-irreducible holds "/\"((uparrow p)\{p},L) <> p proof let L be non empty RelStr; let p be Element of L; assume p is completely-irreducible; then ex_min_of (uparrow p)\{p},L by Def3; then "/\"((uparrow p)\{p},L) in (uparrow p)\{p} by WAYBEL_1:def 4; then not "/\"((uparrow p)\{p},L) in {p} by XBOOLE_0:def 4; hence "/\"((uparrow p)\{p},L) <> p by TARSKI:def 1; end; definition :: DEFINITION 4.19 let L be non empty RelStr; func Irr L -> Subset of L means :Def4: for x be Element of L holds x in it iff x is completely-irreducible; existence proof defpred P[Element of L] means $1 is completely-irreducible; consider X be Subset of L such that A1: for x be Element of L holds x in X iff P[x] from SSubsetEx; take X; thus thesis by A1; end; uniqueness proof let S1,S2 be Subset of L such that A2: for x be Element of L holds x in S1 iff x is completely-irreducible and A3: for x be Element of L holds x in S2 iff x is completely-irreducible; now let x1 be set; thus x1 in S1 implies x1 in S2 proof assume A4: x1 in S1; then reconsider x2 = x1 as Element of L; x2 is completely-irreducible by A2,A4; hence x1 in S2 by A3; end; thus x1 in S2 implies x1 in S1 proof assume A5: x1 in S2; then reconsider x2 = x1 as Element of L; x2 is completely-irreducible by A3,A5; hence x1 in S1 by A2; end; end; hence S1 = S2 by TARSKI:2; end; end; theorem Th20: :: THEOREM 4.19 (i) for L be non empty Poset for p be Element of L holds p is completely-irreducible iff ex q be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & uparrow p = {p} \/ uparrow q proof let L be non empty Poset; let p be Element of L; thus p is completely-irreducible implies ex q be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & uparrow p = {p} \/ uparrow q proof assume A1: p is completely-irreducible; then A2: ex_min_of (uparrow p)\{p},L by Def3; A3: "/\"((uparrow p)\{p},L) <> p by A1,Th19; take q = "/\" ((uparrow p)\{p},L); A4: ex_inf_of (uparrow p)\{p},L by A2,WAYBEL_1:def 4; then A5: q is_<=_than (uparrow p)\{p} by YELLOW_0:def 10; now let s be Element of L; assume s in (uparrow p)\{p}; then s in uparrow p by XBOOLE_0:def 4; hence p <= s by WAYBEL_0:18; end; then p is_<=_than (uparrow p)\{p} by LATTICE3:def 8; then A6: p <= q by A4,YELLOW_0:def 10; hence p < q by A3,ORDERS_1:def 10; thus for s be Element of L st p < s holds q <= s proof let s be Element of L; assume A7: p < s; then A8: not s in {p} by TARSKI:def 1; p <= s by A7,ORDERS_1:def 10; then s in uparrow p by WAYBEL_0:18; then s in (uparrow p)\{p} by A8,XBOOLE_0:def 4; hence q <= s by A5,LATTICE3:def 8; end; thus uparrow p = {p} \/ uparrow q proof thus uparrow p c= {p} \/ uparrow q proof let x be set; assume A9: x in uparrow p; then reconsider x1 = x as Element of L; p = x1 or (x1 in uparrow p & not x1 in {p}) by A9,TARSKI:def 1; then p = x1 or x1 in (uparrow p)\{p} by XBOOLE_0:def 4; then p = x1 or "/\" ((uparrow p)\{p},L) <= x1 by A5,LATTICE3:def 8; then x in {p} or x in uparrow q by TARSKI:def 1,WAYBEL_0:18; hence x in {p} \/ uparrow q by XBOOLE_0:def 2; end; thus {p} \/ uparrow q c= uparrow p proof let x be set; assume A10: x in {p} \/ uparrow q; now per cases by A10,XBOOLE_0:def 2; suppose x in {p}; then x = p & p <= p by TARSKI:def 1; hence x in uparrow p by WAYBEL_0:18; suppose A11: x in uparrow q; then reconsider x1 = x as Element of L; q <= x1 by A11,WAYBEL_0:18; then p <= x1 by A6,ORDERS_1:26; hence x in uparrow p by WAYBEL_0:18; end; hence x in uparrow p; end; end; end; thus (ex q be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & uparrow p = {p} \/ uparrow q) implies p is completely-irreducible proof given q be Element of L such that A12: p < q and A13: for s be Element of L st p < s holds q <= s and A14: uparrow p = {p} \/ uparrow q; ex q be Element of L st (uparrow p)\{p} is_>=_than q & for b be Element of L st (uparrow p)\{p} is_>=_than b holds q >= b proof take q; now let a be Element of L; assume a in (uparrow p)\{p}; then a in uparrow p & not a in {p} by XBOOLE_0:def 4; then p <= a & a <> p by TARSKI:def 1,WAYBEL_0:18; then p < a by ORDERS_1:def 10; hence q <= a by A13; end; hence (uparrow p)\{p} is_>=_than q by LATTICE3:def 8; let b be Element of L; assume A15: (uparrow p)\{p} is_>=_than b; q <> p & q <= q by A12; then q in uparrow q & q <> p by WAYBEL_0:18; then q in {p} \/ uparrow q & not q in {p} by TARSKI:def 1,XBOOLE_0:def 2 ; then q in (uparrow p)\{p} by A14,XBOOLE_0:def 4; hence q >= b by A15,LATTICE3:def 8; end; then A16: ex_inf_of (uparrow p)\{p},L by YELLOW_0:16; now let c be Element of L; assume c in (uparrow p)\{p}; then c in uparrow p & not c in {p} by XBOOLE_0:def 4; then c in uparrow q by A14,XBOOLE_0:def 2; hence q <= c by WAYBEL_0:18; end; then A17: q is_<=_than (uparrow p)\{p} by LATTICE3:def 8; now let b be Element of L; assume A18: b is_<=_than (uparrow p)\{p}; p <= q & p <> q by A12,ORDERS_1:def 10; then q in uparrow p & not q in {p} by TARSKI:def 1,WAYBEL_0:18; then q in (uparrow p)\{p} by XBOOLE_0:def 4; hence q >= b by A18,LATTICE3:def 8; end; then A19: q = "/\"((uparrow p)\{p},L) by A17,YELLOW_0:31; p <= q & p <> q by A12,ORDERS_1:def 10; then q in uparrow p & not q in {p} by TARSKI:def 1,WAYBEL_0:18; then "/\"((uparrow p)\{p},L) in (uparrow p)\{p} by A19,XBOOLE_0:def 4; then ex_min_of (uparrow p)\{p},L by A16,WAYBEL_1:def 4; hence p is completely-irreducible by Def3; end; end; theorem Th21: :: THEOREM 4.19 (ii) for L be upper-bounded non empty Poset holds not Top L in Irr L proof let L be upper-bounded non empty Poset; assume Top L in Irr L; then Top L is completely-irreducible by Def4; then "/\" ((uparrow Top L)\{Top L},L) <> Top L by Th19; then "/\" ({Top L}\{Top L},L) <> Top L by WAYBEL_4:24; then "/\" ({},L) <> Top L by XBOOLE_1:37; hence contradiction by YELLOW_0:def 12; end; theorem Th22: :: THEOREM 4.19 (iii) for L be Semilattice holds Irr L c= IRR L proof let L be Semilattice; let x be set; assume A1: x in Irr L; then reconsider x1 = x as Element of L; x1 is completely-irreducible by A1,Def4; then consider q be Element of L such that A2: x1 < q and A3: for s be Element of L st x1 < s holds q <= s and uparrow x1 = {x1} \/ uparrow q by Th20; now let a,b be Element of L; assume that A4: x1 = a "/\" b and A5: a <> x1 and A6: b <> x1; x1 <= a & x1 <= b by A4,YELLOW_0:23; then x1 < a & x1 < b by A5,A6,ORDERS_1:def 10; then q <= a & q <= b by A3; then A7: q <= x1 by A4,YELLOW_0:23; x1 <= q & x1 <> q by A2,ORDERS_1:def 10; hence contradiction by A7,ORDERS_1:25; end; then x1 is irreducible by WAYBEL_6:def 2; hence x in IRR L by WAYBEL_6:def 4; end; theorem Th23: for L be Semilattice for x be Element of L holds x is completely-irreducible implies x is irreducible proof let L be Semilattice; let x be Element of L; A1: Irr L c= IRR L by Th22; assume x is completely-irreducible; then x in Irr L by Def4; hence x is irreducible by A1,WAYBEL_6:def 4; end; theorem Th24: for L be non empty Poset for x be Element of L holds x is completely-irreducible implies for X be Subset of L st ex_inf_of X,L & x = inf X holds x in X proof let L be non empty Poset; let x be Element of L; assume x is completely-irreducible; then consider q be Element of L such that A1: x < q and A2: for s be Element of L st x < s holds q <= s and uparrow x = {x} \/ uparrow q by Th20; let X be Subset of L; assume that A3: ex_inf_of X,L and A4: x = inf X and A5: not x in X; A6: ex_inf_of uparrow q,L by WAYBEL_0:39; X c= uparrow q proof let y be set; assume A7: y in X; then reconsider y1 = y as Element of L; inf X is_<=_than X by A3,YELLOW_0:31; then x <= y1 by A4,A7,LATTICE3:def 8; then x < y1 by A5,A7,ORDERS_1:def 10; then q <= y1 by A2; hence y in uparrow q by WAYBEL_0:18; end; then inf (uparrow q) <= inf X by A3,A6,YELLOW_0:35; then q <= x by A4,WAYBEL_0:39; hence contradiction by A1,ORDERS_1:30; end; theorem Th25: :: REMARK 4.20 for L be non empty Poset for X be Subset of L st X is order-generating holds Irr L c= X proof let L be non empty Poset; let X be Subset of L; assume A1: X is order-generating; let x be set; assume A2: x in Irr L; then reconsider x1 = x as Element of L; A3: x1 = "/\" ((uparrow x1) /\ X,L) by A1,WAYBEL_6:def 5; A4: x1 is completely-irreducible by A2,Def4; ex_inf_of (uparrow x1) /\ X,L by A1,WAYBEL_6:def 5; then x1 in (uparrow x1) /\ X by A3,A4,Th24; hence x in X by XBOOLE_0:def 3; end; theorem Th26: :: PROPOSITION 4.21 (i) for L be complete LATTICE for p be Element of L holds (ex k be Element of L st p is_maximal_in (the carrier of L) \ uparrow k) implies p is completely-irreducible proof let L be complete LATTICE; let p be Element of L; given k be Element of L such that A1: p is_maximal_in (the carrier of L) \ uparrow k; A2: (uparrow p) \ {p} = (uparrow p) /\ (uparrow k) by A1,Th3; then A3: "/\" ((uparrow p) \ {p},L) = p "\/" k by Th1; A4: ex_inf_of (uparrow p) \ {p},L by YELLOW_0:17; p <= p "\/" k & k <= p "\/" k by YELLOW_0:22; then p "\/" k in uparrow p & p "\/" k in uparrow k by WAYBEL_0:18; then p "\/" k in (uparrow p) /\ (uparrow k) by XBOOLE_0:def 3; then ex_min_of (uparrow p) \ {p},L by A2,A3,A4,WAYBEL_1:def 4; hence p is completely-irreducible by Def3; end; theorem Th27: for L be transitive antisymmetric with_suprema RelStr for p,q,u be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & not u <= p holds p "\/" u = q "\/" u proof let L be transitive antisymmetric with_suprema RelStr; let p,q,u be Element of L; assume that A1: p < q and A2: for s be Element of L st p < s holds q <= s and A3: not u <= p; A4: p <= q by A1,ORDERS_1:def 10; q "\/" u >= q by YELLOW_0:22; then A5: q "\/" u >= p by A4,ORDERS_1:26; A6: q "\/" u >= u by YELLOW_0:22; now let v be Element of L; assume that A7: v >= p and A8: v >= u; v > p by A3,A7,A8,ORDERS_1:def 10; then v >= q by A2; hence q "\/" u <= v by A8,YELLOW_0:22; end; hence p "\/" u = q "\/" u by A5,A6,YELLOW_0:22; end; theorem Th28: for L be distributive LATTICE for p,q,u be Element of L st p < q & (for s be Element of L st p < s holds q <= s) & not u <= p holds not u "/\" q <= p proof let L be distributive LATTICE; let p,q,u be Element of L; assume that A1: p < q and A2: for s be Element of L st p < s holds q <= s and A3: not u <= p and A4: u "/\" q <= p; A5: p <= q by A1,ORDERS_1:def 10; p = p "\/" (u "/\" q) by A4,YELLOW_0:24 .= (p "\/" u) "/\" (q "\/" p) by WAYBEL_1:6 .= (p "\/" u) "/\" q by A5,YELLOW_0:24 .= q "/\" (q "\/" u) by A1,A2,A3,Th27 .= q by LATTICE3:18; hence contradiction by A1; end; theorem Th29: for L be distributive complete LATTICE st L opp is meet-continuous for p be Element of L st p is completely-irreducible holds (the carrier of L) \ downarrow p is Open Filter of L proof let L be distributive complete LATTICE; assume L opp is meet-continuous; then A1: L opp is satisfying_MC by WAYBEL_2:def 7; let p be Element of L; assume A2: p is completely-irreducible; not Top L in Irr L by Th21; then A3: p <> Top L by A2,Def4; p is irreducible by A2,Th23; then p is prime by WAYBEL_6:27; then (downarrow p)` is Filter of L by A3,WAYBEL_6:26; then (downarrow p)` is Filter of L; then reconsider V = (the carrier of L) \ downarrow p as Filter of L by SUBSET_1:def 5 ; consider q be Element of L such that A4: p < q and A5: for s be Element of L st p < s holds q <= s and uparrow p = {p} \/ uparrow q by A2,Th20; defpred P[Element of L] means $1 <= q & not $1 <= p; reconsider F = { t where t is Element of L : P[t]} as Subset of L from RelStrSubset; not q <= p by A4,ORDERS_1:30; then A6: q in F; now let x,y be Element of L; assume that A7: x in F and A8: y in F; take z = x "/\" y; consider x1 be Element of L such that A9: x1 = x and A10: x1 <= q and A11: not x1 <= p by A7; consider y1 be Element of L such that A12: y1 = y and A13: y1 <= q and A14: not y1 <= p by A8; A15: z <= x by YELLOW_0:23; then A16: z <= q by A9,A10,ORDERS_1:26; not z <= p proof assume A17: z <= p; A18: q >= p by A4,ORDERS_1:def 10; A19: now let d be Element of L; assume that A20: d >= y and A21: d >= p; d > p by A12,A14,A20,A21,ORDERS_1:def 10; hence q <= d by A5; end; x = x "/\" q by A9,A10,YELLOW_0:25 .= x "/\" (y "\/" p) by A12,A13,A18,A19,YELLOW_0:22 .= z "\/" (x "/\" p) by WAYBEL_1:def 3 .= (x "\/" z) "/\" (z "\/" p) by WAYBEL_1:6 .= x "/\" (p "\/" z) by A15,YELLOW_0:24 .= x "/\" p by A17,YELLOW_0:24; hence contradiction by A9,A11,YELLOW_0:25; end; hence z in F by A16; thus z <= x by YELLOW_0:23; thus z <= y by YELLOW_0:23; end; then reconsider F as non empty filtered Subset of L by A6,WAYBEL_0:def 2; reconsider F1 = F as non empty directed Subset of L opp by YELLOW_7:27; now let x be Element of L; assume A22: x in V; take y = inf F; thus y in V proof ex_inf_of F,L by YELLOW_0:17; then A23: inf F = sup F1 by YELLOW_7:13; A24: ex_inf_of {p~} "/\" F1,L by YELLOW_0:17; A25: {p~} = {p} by LATTICE3:def 6; assume not y in V; then y in downarrow p by XBOOLE_0:def 4; then y <= p by WAYBEL_0:17; then A26: p = p "\/" y by YELLOW_0:24 .= p~ "/\" (inf F)~ by YELLOW_7:23 .= p~ "/\" sup F1 by A23,LATTICE3:def 6 .= sup ({p~} "/\" F1) by A1,WAYBEL_2:def 6 .= "/\"({p~} "/\" F1,L) by A24,YELLOW_7:13 .= "/\"({p} "\/" F,L) by A25,Th5; now let r be Element of L; assume r in {p} "\/" F; then r in {p "\/" v where v is Element of L : v in F} by YELLOW_4:15; then consider v be Element of L such that A27: r = p "\/" v and A28: v in F; A29: p <= r by A27,YELLOW_0:22; consider v1 be Element of L such that A30: v = v1 and v1 <= q and A31: not v1 <= p by A28; p <> r by A27,A30,A31,YELLOW_0:24; then p < r by A29,ORDERS_1:def 10; hence q <= r by A5; end; then q is_<=_than {p} "\/" F by LATTICE3:def 8; then q <= p by A26,YELLOW_0:33; hence contradiction by A4,ORDERS_1:30; end; then not y in downarrow p by XBOOLE_0:def 4; then A32: not y <= p by WAYBEL_0:17; A33: x "/\" q <= x by YELLOW_0:23; A34: y is_<=_than F by YELLOW_0:33; A35: x "/\" q <= q by YELLOW_0:23; not x in downarrow p by A22,XBOOLE_0:def 4; then not x <= p by WAYBEL_0:17; then not x "/\" q <= p by A4,A5,Th28; then x "/\" q in F by A35; then y <= x "/\" q by A34,LATTICE3:def 8; then A36: y <= x by A33,ORDERS_1:26; now let D be non empty directed Subset of L; assume A37: y <= sup D; D \ downarrow p is non empty proof assume D \ downarrow p is empty; then D c= downarrow p by XBOOLE_1:37; then sup D <= sup (downarrow p) by WAYBEL_7:3; then y <= sup (downarrow p) by A37,ORDERS_1:26; hence contradiction by A32,WAYBEL_0:34; end; then consider d be set such that A38: d in D \ downarrow p by XBOOLE_0:def 1; reconsider d as Element of L by A38; take d; thus d in D by A38,XBOOLE_0:def 4; A39: d "/\" q <= d & d "/\" q <= q by YELLOW_0:23; A40: y is_<=_than F by YELLOW_0:33; not d in downarrow p by A38,XBOOLE_0:def 4; then not d <= p by WAYBEL_0:17; then not d "/\" q <= p by A4,A5,Th28; then d "/\" q in F by A39; then y <= d "/\" q by A40,LATTICE3:def 8; hence y <= d by A39,ORDERS_1:26; end; then y << y by WAYBEL_3:def 1; hence y << x by A36,WAYBEL_3:2; end; hence (the carrier of L) \ downarrow p is Open Filter of L by WAYBEL_6:def 1; end; theorem :: PROPOSITION 4.21 (ii) for L be distributive complete LATTICE st L opp is meet-continuous for p be Element of L holds p is completely-irreducible implies (ex k be Element of L st k in the carrier of CompactSublatt L & p is_maximal_in (the carrier of L) \ uparrow k) proof let L be distributive complete LATTICE; assume A1: L opp is meet-continuous; let p be Element of L; assume A2: p is completely-irreducible; then reconsider V = (the carrier of L) \ downarrow p as Open Filter of L by A1,Th29; reconsider V' = V as non empty directed Subset of L opp by YELLOW_7:27; take k = inf V; A3: L opp is satisfying_MC by A1,WAYBEL_2:def 7; A4: ex_inf_of V,L & ex_inf_of {p~} "/\" V',L by YELLOW_0:17; A5: ex_inf_of {p} "\/" V,L & ex_inf_of (uparrow p) \ {p},L by YELLOW_0:17; A6: (inf V)~ = inf V by LATTICE3:def 6; A7: p = p~ by LATTICE3:def 6; A8: {p} "\/" V c= (uparrow p) \ {p} proof let x be set; assume x in {p} "\/" V; then x in {p "\/" v where v is Element of L: v in V} by YELLOW_4:15; then consider v be Element of L such that A9: x = p "\/" v and A10: v in V; not v in downarrow p by A10,XBOOLE_0:def 4; then not v <= p by WAYBEL_0:17; then p <= p "\/" v & p "\/" v <> p by YELLOW_0:22; then p "\/" v in uparrow p & not p "\/" v in {p} by TARSKI:def 1,WAYBEL_0:18; hence x in (uparrow p) \ {p} by A9,XBOOLE_0:def 4; end; p "\/" k = (p~) "/\" (inf V)~ by YELLOW_7:23 .= (p~) "/\" "\/"(V,L opp) by A4,A6,YELLOW_7:13 .= "\/"({p~} "/\" V',L opp) by A3,WAYBEL_2:def 6 .= "/\"({p~} "/\" V',L) by A4,YELLOW_7:13 .= inf ({p} "\/" V) by A7,Th5; then A11: "/\"((uparrow p) \ {p},L) <= p "\/" k by A5,A8,YELLOW_0:35; A12: "/\"((uparrow p) \ {p},L) <> p by A2,Th19; now let b be Element of L; assume b in (uparrow p) \ {p}; then b in uparrow p by XBOOLE_0:def 4; hence p <= b by WAYBEL_0:18; end; then p is_<=_than (uparrow p) \ {p} by LATTICE3:def 8; then p <= "/\"((uparrow p) \ {p},L) by YELLOW_0:33; then A13: p < "/\"((uparrow p) \ {p},L) by A12,ORDERS_1:def 10; A14: not k <= p proof assume k <= p; then p "\/" k = p by YELLOW_0:24; hence contradiction by A11,A13,ORDERS_1:32; end; uparrow k = V proof thus uparrow k c= V proof let x be set; assume A15: x in uparrow k; then reconsider x1 = x as Element of L; k <= x1 by A15,WAYBEL_0:18; then not x1 <= p by A14,ORDERS_1:26; then not x1 in downarrow p by WAYBEL_0:17; hence x in V by XBOOLE_0:def 4; end; let x be set; assume A16: x in V; then reconsider x1 = x as Element of L; k is_<=_than V by YELLOW_0:33; then k <= x1 by A16,LATTICE3:def 8; hence x in uparrow k by WAYBEL_0:18; end; then k is compact by WAYBEL_8:2; hence k in the carrier of CompactSublatt L by WAYBEL_8:def 1; not p in uparrow k by A14,WAYBEL_0:18; then A17: p in (the carrier of L) \ uparrow k by XBOOLE_0:def 4; not ex y be Element of L st y in (the carrier of L) \ uparrow k & p < y proof given y be Element of L such that A18: y in (the carrier of L) \ uparrow k and A19: p < y; A20: k is_<=_than V by YELLOW_0:33; not y in uparrow k by A18,XBOOLE_0:def 4; then not k <= y by WAYBEL_0:18; then not y in V by A20,LATTICE3:def 8; then y in downarrow p by XBOOLE_0:def 4; then y <= p by WAYBEL_0:17; hence contradiction by A19,ORDERS_1:30; end; hence p is_maximal_in (the carrier of L) \ uparrow k by A17,WAYBEL_4:56; end; theorem Th31: :: THEOREM 4.22 for L be lower-bounded algebraic LATTICE for x,y be Element of L holds not y <= x implies ex p be Element of L st p is completely-irreducible & x <= p & not y <= p proof let L be lower-bounded algebraic LATTICE; let x,y be Element of L; A1: for z be Element of L holds waybelow z is non empty directed; assume not y <= x; then consider k1 be Element of L such that A2: k1 << y and A3: not k1 <= x by A1,WAYBEL_3:24; consider k be Element of L such that A4: k in the carrier of CompactSublatt L and A5: k1 <= k and A6: k <= y by A2,WAYBEL_8:7; not k <= x by A3,A5,ORDERS_1:26; then not x in uparrow k by WAYBEL_0:18; then x in (the carrier of L) \ (uparrow k) by XBOOLE_0:def 4; then x in (uparrow k)` by SUBSET_1:def 5; then A7: x in (uparrow k)`; k is compact by A4,WAYBEL_8:def 1; then uparrow k is Open Filter of L by WAYBEL_8:2; then consider p be Element of L such that A8: x <= p and A9: p is_maximal_in ((uparrow k)`) by A7,WAYBEL_6:9; take p; (the carrier of L) \ uparrow k = (uparrow k)` by SUBSET_1:def 5; hence p is completely-irreducible by A9,Th26; thus x <= p by A8; thus not y <= p proof assume y <= p; then A10: k <= p by A6,ORDERS_1:26; p in (uparrow k)` by A9,WAYBEL_4:56; then p in (uparrow k)`; then p in (the carrier of L) \ uparrow k by SUBSET_1:def 5; then not p in uparrow k by XBOOLE_0:def 4; hence contradiction by A10,WAYBEL_0:18; end; end; theorem Th32: :: THEOREM 4.23 (i) for L be lower-bounded algebraic LATTICE holds Irr L is order-generating & for X be Subset of L st X is order-generating holds Irr L c= X proof let L be lower-bounded algebraic LATTICE; now let x,y be Element of L; assume not y <= x; then consider p be Element of L such that A1: p is completely-irreducible and A2: x <= p and A3: not y <= p by Th31; take p; thus p in Irr L by A1,Def4; thus x <= p by A2; thus not y <= p by A3; end; hence Irr L is order-generating by WAYBEL_6:17; let X be Subset of L; assume X is order-generating; hence Irr L c= X by Th25; end; theorem :: THEOREM 4.23 (ii) for L be lower-bounded algebraic LATTICE for s be Element of L holds s = "/\" (uparrow s /\ Irr L,L) proof let L be lower-bounded algebraic LATTICE; let s be Element of L; Irr L is order-generating by Th32; hence s = "/\" (uparrow s /\ Irr L,L) by WAYBEL_6:def 5; end; theorem Th34: for L be complete (non empty Poset) for X be Subset of L for p be Element of L st p is completely-irreducible & p = inf X holds p in X proof let L be complete (non empty Poset); let X be Subset of L; let p be Element of L; assume that A1: p is completely-irreducible and A2: p = inf X; consider q be Element of L such that A3: p < q and A4: for s be Element of L st p < s holds q <= s and uparrow p = {p} \/ uparrow q by A1,Th20; assume A5: not p in X; A6: p is_<=_than X & for b be Element of L st b is_<=_than X holds p >= b by A2,YELLOW_0:33; A7: p <= q by A3,ORDERS_1:def 10; now let b be Element of L; assume A8: b in X; then p <= b by A6,LATTICE3:def 8; then p < b by A5,A8,ORDERS_1:def 10; hence q <= b by A4; end; then A9: q is_<=_than X by LATTICE3:def 8; now let b be Element of L; assume b is_<=_than X; then p >= b by A2,YELLOW_0:33; hence q >= b by A7,ORDERS_1:26; end; hence contradiction by A2,A3,A9,YELLOW_0:33; end; theorem Th35: for L be complete algebraic LATTICE for p be Element of L st p is completely-irreducible holds p = "/\" ({ x where x is Element of L : x in uparrow p & ex k be Element of L st k in the carrier of CompactSublatt L & x is_maximal_in (the carrier of L) \ uparrow k },L) proof let L be complete algebraic LATTICE; let p be Element of L; set A = { x where x is Element of L : x in uparrow p & ex k be Element of L st k in the carrier of CompactSublatt L & x is_maximal_in (the carrier of L) \ uparrow k }; assume p is completely-irreducible; then consider q be Element of L such that A1: p < q and A2: for s be Element of L st p < s holds q <= s and uparrow p = {p} \/ uparrow q by Th20; p <= q by A1,ORDERS_1:def 10; then A3: compactbelow p c= compactbelow q by WAYBEL13:1; compactbelow p <> compactbelow q proof assume compactbelow p = compactbelow q; then p = sup compactbelow q by WAYBEL_8:def 3 .= q by WAYBEL_8:def 3; hence contradiction by A1; end; then not compactbelow q c= compactbelow p by A3,XBOOLE_0:def 10; then consider k1 be set such that A4: k1 in compactbelow q and A5: not k1 in compactbelow p by TARSKI:def 3; k1 in { y where y is Element of L: q >= y & y is compact } by A4,WAYBEL_8:def 2; then consider k be Element of L such that A6: k = k1 and A7: q >= k and A8: k is compact; A9: k in the carrier of CompactSublatt L by A8,WAYBEL_8:def 1; p <= p; then A10: p in uparrow p by WAYBEL_0:18; not k <= p by A5,A6,A8,WAYBEL_8:4; then not p in uparrow k by WAYBEL_0:18; then A11: p in (the carrier of L) \ uparrow k by XBOOLE_0:def 4; not ex y be Element of L st y in (the carrier of L) \ uparrow k & p < y proof given y be Element of L such that A12: y in (the carrier of L) \ uparrow k and A13: p < y; q <= y by A2,A13; then k <= y by A7,ORDERS_1:26; then y in uparrow k by WAYBEL_0:18; hence contradiction by A12,XBOOLE_0:def 4; end; then p is_maximal_in (the carrier of L) \ uparrow k by A11,WAYBEL_4:56; then A14: p in A by A9,A10; now let a be Element of L; assume a in A; then consider a1 be Element of L such that A15: a1 = a and A16: a1 in uparrow p and ex k be Element of L st k in the carrier of CompactSublatt L & a1 is_maximal_in (the carrier of L) \ uparrow k; thus p <= a by A15,A16,WAYBEL_0:18; end; then A17: p is_<=_than A by LATTICE3:def 8; for u be Element of L st u is_<=_than A holds p >= u by A14,LATTICE3:def 8; hence p = "/\"(A,L) by A17,YELLOW_0:33; end; theorem :: COROLLARY 4.24 for L be complete algebraic LATTICE for p be Element of L holds (ex k be Element of L st k in the carrier of CompactSublatt L & p is_maximal_in (the carrier of L) \ uparrow k) iff p is completely-irreducible proof let L be complete algebraic LATTICE; let p be Element of L; thus (ex k be Element of L st k in the carrier of CompactSublatt L & p is_maximal_in (the carrier of L) \ uparrow k) implies p is completely-irreducible by Th26; thus p is completely-irreducible implies (ex k be Element of L st k in the carrier of CompactSublatt L & p is_maximal_in (the carrier of L) \ uparrow k) proof defpred P[Element of L] means $1 in uparrow p & ex k be Element of L st k in the carrier of CompactSublatt L & $1 is_maximal_in (the carrier of L) \ uparrow k; reconsider A = { x where x is Element of L : P[x]} as Subset of L from RelStrSubset; assume A1: p is completely-irreducible; then p = inf A by Th35; then p in A by A1,Th34; then consider x be Element of L such that A2: x = p and x in uparrow p and A3: ex k be Element of L st k in the carrier of CompactSublatt L & x is_maximal_in (the carrier of L) \ uparrow k; consider k be Element of L such that A4: k in the carrier of CompactSublatt L and A5: x is_maximal_in (the carrier of L) \ uparrow k by A3; take k; thus k in the carrier of CompactSublatt L by A4; thus p is_maximal_in (the carrier of L) \ uparrow k by A2,A5; end; end;

Back to top