:: Completely-Irreducible Elements :: by Robert Milewski :: :: Received February 9, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies WAYBEL_0, SUBSET_1, LATTICES, XBOOLE_0, EQREL_1, ORDERS_2, ORDERS_1, STRUCT_0, XXREAL_0, TARSKI, ARYTM_3, LATTICE3, ARYTM_0, RELAT_1, RELAT_2, CARD_FIL, REWRITE1, FUNCT_1, FUNCOP_1, YELLOW_0, SEQM_3, FINSET_1, ORDINAL2, YELLOW_1, SETFAM_1, WELLORD2, ZFMISC_1, WAYBEL_1, WAYBEL_6, YELLOW_8, WAYBEL_2, INT_2, WAYBEL_3, WAYBEL_8, RCOMP_1, WAYBEL16; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, RELSET_1, FUNCT_2, FUNCOP_1, DOMAIN_1, ORDERS_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_4, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_8; constructors DOMAIN_1, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_6, WAYBEL_8, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, WAYBEL_3, YELLOW_7, WAYBEL_6, WAYBEL_8; requirements BOOLE, SUBSET; begin :: Preliminaries theorem :: WAYBEL16:1 for L be sup-Semilattice for x,y be Element of L holds "/\"(( uparrow x) /\ (uparrow y),L) = x "\/" y; theorem :: WAYBEL16:2 for L be Semilattice for x,y be Element of L holds "\/"((downarrow x) /\ (downarrow y),L) = x "/\" y; theorem :: WAYBEL16:3 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); theorem :: WAYBEL16:4 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); theorem :: WAYBEL16:5 for L be with_suprema Poset for X,Y be Subset of L for X9,Y9 be Subset of L opp st X = X9 & Y = Y9 holds X "\/" Y = X9 "/\" Y9; theorem :: WAYBEL16:6 for L be with_infima Poset for X,Y be Subset of L for X9,Y9 be Subset of L opp st X = X9 & Y = Y9 holds X "/\" Y = X9 "\/" Y9; theorem :: WAYBEL16:7 for L be non empty reflexive transitive RelStr holds Filt L = Ids (L opp); theorem :: WAYBEL16:8 for L be non empty reflexive transitive RelStr holds Ids L = Filt (L opp); begin :: Free Generation Set definition let S,T be complete non empty Poset; mode CLHomomorphism of S,T -> Function of S,T means :: WAYBEL16:def 1 it is directed-sups-preserving infs-preserving; end; definition let S be continuous complete non empty Poset; let A be Subset of S; pred A is_FG_set means :: WAYBEL16:def 2 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 h9 be CLHomomorphism of S,T st h9|A = f holds h9 = h; end; registration let L be upper-bounded non empty Poset; cluster Filt L -> non empty; end; theorem :: WAYBEL16:9 for X be set for Y be non empty Subset of InclPoset Filt BoolePoset X holds meet Y is Filter of BoolePoset X; theorem :: WAYBEL16:10 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; theorem :: WAYBEL16:11 for X be set holds bool X is Filter of BoolePoset X; theorem :: WAYBEL16:12 for X be set holds {X} is Filter of BoolePoset X; theorem :: WAYBEL16:13 for X be set holds InclPoset Filt BoolePoset X is upper-bounded; theorem :: WAYBEL16:14 for X be set holds InclPoset Filt BoolePoset X is lower-bounded; theorem :: WAYBEL16:15 for X be set holds Top (InclPoset Filt BoolePoset X) = bool X; theorem :: WAYBEL16:16 for X be set holds Bottom (InclPoset Filt BoolePoset X) = {X}; theorem :: WAYBEL16:17 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; theorem :: WAYBEL16:18 for L be upper-bounded Semilattice holds InclPoset Filt L is complete; registration let L be upper-bounded Semilattice; cluster InclPoset Filt L -> complete; end; begin :: Completely-irreducible Elements definition let L be non empty RelStr; let p be Element of L; attr p is completely-irreducible means :: WAYBEL16:def 3 ex_min_of (uparrow p)\{p},L; end; theorem :: WAYBEL16:19 for L be non empty RelStr for p be Element of L st p is completely-irreducible holds "/\"((uparrow p)\{p},L) <> p; definition let L be non empty RelStr; func Irr L -> Subset of L means :: WAYBEL16:def 4 for x be Element of L holds x in it iff x is completely-irreducible; end; theorem :: WAYBEL16:20 :: 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; theorem :: WAYBEL16:21 :: THEOREM 4.19 (ii) for L be upper-bounded non empty Poset holds not Top L in Irr L; theorem :: WAYBEL16:22 :: THEOREM 4.19 (iii) for L be Semilattice holds Irr L c= IRR L; theorem :: WAYBEL16:23 for L be Semilattice for x be Element of L holds x is completely-irreducible implies x is irreducible; theorem :: WAYBEL16:24 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; theorem :: WAYBEL16:25 :: 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; theorem :: WAYBEL16:26 :: 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; theorem :: WAYBEL16:27 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; theorem :: WAYBEL16:28 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; theorem :: WAYBEL16:29 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; theorem :: WAYBEL16:30 :: 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; theorem :: WAYBEL16:31 :: 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; theorem :: WAYBEL16:32 :: 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; theorem :: WAYBEL16:33 :: THEOREM 4.23 (ii) for L be lower-bounded algebraic LATTICE for s be Element of L holds s = "/\" (uparrow s /\ Irr L,L); theorem :: WAYBEL16:34 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; theorem :: WAYBEL16:35 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); theorem :: WAYBEL16:36 :: 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;