:: Completely-Irreducible Elements :: by Robert Milewski :: :: Received February 9, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin theorem Th1: :: WAYBEL16:1 for L being sup-Semilattice for x, y being Element of L holds "/\" (((uparrow x) /\ (uparrow y)),L) = x "\/" y proofend; theorem :: WAYBEL16:2 for L being Semilattice for x, y being Element of L holds "\/" (((downarrow x) /\ (downarrow y)),L) = x "/\" y proofend; theorem Th3: :: WAYBEL16:3 for L being non empty RelStr for x, y being Element of L st x is_maximal_in the carrier of L \ (uparrow y) holds (uparrow x) \ {x} = (uparrow x) /\ (uparrow y) proofend; theorem :: WAYBEL16:4 for L being non empty RelStr for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds (downarrow x) \ {x} = (downarrow x) /\ (downarrow y) proofend; theorem Th5: :: WAYBEL16:5 for L being with_suprema Poset for X, Y being Subset of L for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds X "\/" Y = X9 "/\" Y9 proofend; theorem :: WAYBEL16:6 for L being with_infima Poset for X, Y being Subset of L for X9, Y9 being Subset of (L opp) st X = X9 & Y = Y9 holds X "/\" Y = X9 "\/" Y9 proofend; theorem Th7: :: WAYBEL16:7 for L being non empty reflexive transitive RelStr holds Filt L = Ids (L opp) proofend; theorem :: WAYBEL16:8 for L being non empty reflexive transitive RelStr holds Ids L = Filt (L opp) proofend; begin definition let S, T be non empty complete Poset; mode CLHomomorphism of S,T -> Function of S,T means :: WAYBEL16:def 1 ( it is directed-sups-preserving & it is infs-preserving ); existence ex b1 being Function of S,T st ( b1 is directed-sups-preserving & b1 is infs-preserving ) proofend; end; :: deftheorem defines CLHomomorphism WAYBEL16:def_1_:_ for S, T being non empty complete Poset for b3 being Function of S,T holds ( b3 is CLHomomorphism of S,T iff ( b3 is directed-sups-preserving & b3 is infs-preserving ) ); definition let S be non empty complete continuous Poset; let A be Subset of S; predA is_FG_set means :: WAYBEL16:def 2 for T being non empty complete continuous Poset for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st ( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds h9 = h ) ); end; :: deftheorem defines is_FG_set WAYBEL16:def_2_:_ for S being non empty complete continuous Poset for A being Subset of S holds ( A is_FG_set iff for T being non empty complete continuous Poset for f being Function of A, the carrier of T ex h being CLHomomorphism of S,T st ( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds h9 = h ) ) ); registration let L be non empty upper-bounded Poset; cluster Filt L -> non empty ; coherence not Filt L is empty proofend; end; theorem Th9: :: WAYBEL16:9 for X being set for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds meet Y is Filter of (BoolePoset X) proofend; theorem :: WAYBEL16:10 for X being set for Y being non empty Subset of (InclPoset (Filt (BoolePoset X))) holds ( ex_inf_of Y, InclPoset (Filt (BoolePoset X)) & "/\" (Y,(InclPoset (Filt (BoolePoset X)))) = meet Y ) proofend; theorem Th11: :: WAYBEL16:11 for X being set holds bool X is Filter of (BoolePoset X) proofend; theorem Th12: :: WAYBEL16:12 for X being set holds {X} is Filter of (BoolePoset X) proofend; theorem :: WAYBEL16:13 for X being set holds InclPoset (Filt (BoolePoset X)) is upper-bounded proofend; theorem :: WAYBEL16:14 for X being set holds InclPoset (Filt (BoolePoset X)) is lower-bounded proofend; theorem :: WAYBEL16:15 for X being set holds Top (InclPoset (Filt (BoolePoset X))) = bool X proofend; theorem :: WAYBEL16:16 for X being set holds Bottom (InclPoset (Filt (BoolePoset X))) = {X} proofend; theorem :: WAYBEL16:17 for X being non empty set for Y being non empty Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds union Y c= sup Y proofend; theorem Th18: :: WAYBEL16:18 for L being upper-bounded Semilattice holds InclPoset (Filt L) is complete proofend; registration let L be upper-bounded Semilattice; cluster InclPoset (Filt L) -> complete ; coherence InclPoset (Filt L) is complete by Th18; end; begin definition let L be non empty RelStr ; let p be Element of L; attrp is completely-irreducible means :Def3: :: WAYBEL16:def 3 ex_min_of (uparrow p) \ {p},L; end; :: deftheorem Def3 defines completely-irreducible WAYBEL16:def_3_:_ for L being non empty RelStr for p being Element of L holds ( p is completely-irreducible iff ex_min_of (uparrow p) \ {p},L ); theorem Th19: :: WAYBEL16:19 for L being non empty RelStr for p being Element of L st p is completely-irreducible holds "/\" (((uparrow p) \ {p}),L) <> p proofend; definition let L be non empty RelStr ; func Irr L -> Subset of L means :Def4: :: WAYBEL16:def 4 for x being Element of L holds ( x in it iff x is completely-irreducible ); existence ex b1 being Subset of L st for x being Element of L holds ( x in b1 iff x is completely-irreducible ) proofend; uniqueness for b1, b2 being Subset of L st ( for x being Element of L holds ( x in b1 iff x is completely-irreducible ) ) & ( for x being Element of L holds ( x in b2 iff x is completely-irreducible ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines Irr WAYBEL16:def_4_:_ for L being non empty RelStr for b2 being Subset of L holds ( b2 = Irr L iff for x being Element of L holds ( x in b2 iff x is completely-irreducible ) ); theorem Th20: :: WAYBEL16:20 for L being non empty Poset for p being Element of L holds ( p is completely-irreducible iff ex q being Element of L st ( p < q & ( for s being Element of L st p < s holds q <= s ) & uparrow p = {p} \/ (uparrow q) ) ) proofend; theorem Th21: :: WAYBEL16:21 for L being non empty upper-bounded Poset holds not Top L in Irr L proofend; theorem Th22: :: WAYBEL16:22 for L being Semilattice holds Irr L c= IRR L proofend; theorem Th23: :: WAYBEL16:23 for L being Semilattice for x being Element of L st x is completely-irreducible holds x is irreducible proofend; theorem Th24: :: WAYBEL16:24 for L being non empty Poset for x being Element of L st x is completely-irreducible holds for X being Subset of L st ex_inf_of X,L & x = inf X holds x in X proofend; theorem Th25: :: WAYBEL16:25 for L being non empty Poset for X being Subset of L st X is order-generating holds Irr L c= X proofend; theorem Th26: :: WAYBEL16:26 for L being complete LATTICE for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds p is completely-irreducible proofend; theorem Th27: :: WAYBEL16:27 for L being transitive antisymmetric with_suprema RelStr for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds q <= s ) & not u <= p holds p "\/" u = q "\/" u proofend; theorem Th28: :: WAYBEL16:28 for L being distributive LATTICE for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds q <= s ) & not u <= p holds not u "/\" q <= p proofend; theorem Th29: :: WAYBEL16:29 for L being distributive complete LATTICE st L opp is meet-continuous holds for p being Element of L st p is completely-irreducible holds the carrier of L \ (downarrow p) is Open Filter of L proofend; theorem :: WAYBEL16:30 for L being distributive complete LATTICE st L opp is meet-continuous holds for p being Element of L st p is completely-irreducible holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & p is_maximal_in the carrier of L \ (uparrow k) ) proofend; theorem Th31: :: WAYBEL16:31 for L being lower-bounded algebraic LATTICE for x, y being Element of L st not y <= x holds ex p being Element of L st ( p is completely-irreducible & x <= p & not y <= p ) proofend; theorem Th32: :: WAYBEL16:32 for L being lower-bounded algebraic LATTICE holds ( Irr L is order-generating & ( for X being Subset of L st X is order-generating holds Irr L c= X ) ) proofend; theorem :: WAYBEL16:33 for L being lower-bounded algebraic LATTICE for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L) proofend; theorem Th34: :: WAYBEL16:34 for L being non empty complete Poset for X being Subset of L for p being Element of L st p is completely-irreducible & p = inf X holds p in X proofend; theorem Th35: :: WAYBEL16:35 for L being complete algebraic LATTICE for p being Element of L st p is completely-irreducible holds p = "/\" ( { x where x is Element of L : ( x in uparrow p & ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x is_maximal_in the carrier of L \ (uparrow k) ) ) } ,L) proofend; theorem :: WAYBEL16:36 for L being complete algebraic LATTICE for p being Element of L holds ( ex k being 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 ) proofend;