:: Irreducible and Prime Elements :: by Beata Madras :: :: Received December 1, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin scheme :: WAYBEL_6:sch 1 NonUniqExD1{ F1() -> non empty RelStr , F2() -> Subset of F1(), F3() -> non empty Subset of F1(), P1[ set , set ] } : ex f being Function of F2(),F3() st for e being Element of F1() st e in F2() holds ex u being Element of F1() st ( u in F3() & u = f . e & P1[e,u] ) provided A1: for e being Element of F1() st e in F2() holds ex u being Element of F1() st ( u in F3() & P1[e,u] ) proofend; definition let L be LATTICE; let A be non empty Subset of L; let f be Function of A,A; let n be Element of NAT ; :: original:iter redefine func iter (f,n) -> Function of A,A; coherence iter (f,n) is Function of A,A by FUNCT_7:83; end; definition let L be LATTICE; let C, D be non empty Subset of L; let f be Function of C,D; let c be Element of C; :: original:. redefine funcf . c -> Element of L; coherence f . c is Element of L proofend; end; registration let L be non empty Poset; cluster strongly_connected -> directed filtered for Element of bool the carrier of L; coherence for b1 being Chain of L holds ( b1 is filtered & b1 is directed ) proofend; end; registration cluster non empty strict V110() reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous for RelStr ; existence ex b1 being LATTICE st ( b1 is strict & b1 is continuous & b1 is distributive & b1 is lower-bounded ) proofend; end; theorem Th1: :: WAYBEL_6:1 for S, T being Semilattice for f being Function of S,T holds ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) proofend; theorem Th2: :: WAYBEL_6:2 for S, T being sup-Semilattice for f being Function of S,T holds ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) proofend; theorem Th3: :: WAYBEL_6:3 for S, T being LATTICE for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds S is distributive proofend; registration let S, T be complete LATTICE; cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V32( the carrier of S, the carrier of T) sups-preserving for Element of bool [: the carrier of S, the carrier of T:]; existence ex b1 being Function of S,T st b1 is sups-preserving proofend; end; Lm1: for S, T being non empty with_suprema Poset for f being Function of S,T st f is directed-sups-preserving holds f is monotone proofend; theorem Th4: :: WAYBEL_6:4 for S, T being complete LATTICE for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds S is meet-continuous proofend; begin definition let L be non empty reflexive RelStr ; let X be Subset of L; attrX is Open means :Def1: :: WAYBEL_6:def 1 for x being Element of L st x in X holds ex y being Element of L st ( y in X & y << x ); end; :: deftheorem Def1 defines Open WAYBEL_6:def_1_:_ for L being non empty reflexive RelStr for X being Subset of L holds ( X is Open iff for x being Element of L st x in X holds ex y being Element of L st ( y in X & y << x ) ); theorem :: WAYBEL_6:5 for L being up-complete LATTICE for X being upper Subset of L holds ( X is Open iff for x being Element of L st x in X holds waybelow x meets X ) proofend; theorem :: WAYBEL_6:6 for L being up-complete LATTICE for X being upper Subset of L holds ( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } ) proofend; registration let L be lower-bounded up-complete LATTICE; cluster non empty filtered upper Open for Element of bool the carrier of L; existence ex b1 being Filter of L st b1 is Open proofend; end; theorem :: WAYBEL_6:7 for L being lower-bounded continuous LATTICE for x being Element of L holds wayabove x is Open proofend; theorem Th8: :: WAYBEL_6:8 for L being lower-bounded continuous LATTICE for x, y being Element of L st x << y holds ex F being Open Filter of L st ( y in F & F c= wayabove x ) proofend; theorem Th9: :: WAYBEL_6:9 for L being complete LATTICE for X being upper Open Subset of L for x being Element of L st x in X ` holds ex m being Element of L st ( x <= m & m is_maximal_in X ` ) proofend; begin definition let G be non empty RelStr ; let g be Element of G; attrg is meet-irreducible means :Def2: :: WAYBEL_6:def 2 for x, y being Element of G holds ( not g = x "/\" y or x = g or y = g ); end; :: deftheorem Def2 defines meet-irreducible WAYBEL_6:def_2_:_ for G being non empty RelStr for g being Element of G holds ( g is meet-irreducible iff for x, y being Element of G holds ( not g = x "/\" y or x = g or y = g ) ); notation let G be non empty RelStr ; let g be Element of G; synonym irreducible g for meet-irreducible ; end; definition let G be non empty RelStr ; let g be Element of G; attrg is join-irreducible means :: WAYBEL_6:def 3 for x, y being Element of G holds ( not g = x "\/" y or x = g or y = g ); end; :: deftheorem defines join-irreducible WAYBEL_6:def_3_:_ for G being non empty RelStr for g being Element of G holds ( g is join-irreducible iff for x, y being Element of G holds ( not g = x "\/" y or x = g or y = g ) ); definition let L be non empty RelStr ; func IRR L -> Subset of L means :Def4: :: WAYBEL_6:def 4 for x being Element of L holds ( x in it iff x is irreducible ); existence ex b1 being Subset of L st for x being Element of L holds ( x in b1 iff x is irreducible ) proofend; uniqueness for b1, b2 being Subset of L st ( for x being Element of L holds ( x in b1 iff x is irreducible ) ) & ( for x being Element of L holds ( x in b2 iff x is irreducible ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines IRR WAYBEL_6: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 irreducible ) ); theorem Th10: :: WAYBEL_6:10 for L being non empty antisymmetric upper-bounded with_infima RelStr holds Top L is irreducible proofend; registration let L be non empty antisymmetric upper-bounded with_infima RelStr ; cluster irreducible for Element of the carrier of L; existence ex b1 being Element of L st b1 is irreducible proofend; end; theorem :: WAYBEL_6:11 for L being Semilattice for x being Element of L holds ( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds x in A ) proofend; theorem :: WAYBEL_6:12 for L being LATTICE for l being Element of L st (uparrow l) \ {l} is Filter of L holds l is irreducible proofend; theorem Th13: :: WAYBEL_6:13 for L being LATTICE for p being Element of L for F being Filter of L st p is_maximal_in F ` holds p is irreducible proofend; theorem Th14: :: WAYBEL_6:14 for L being lower-bounded continuous LATTICE for x, y being Element of L st not y <= x holds ex p being Element of L st ( p is irreducible & x <= p & not y <= p ) proofend; begin definition let L be non empty RelStr ; let X be Subset of L; attrX is order-generating means :Def5: :: WAYBEL_6:def 5 for x being Element of L holds ( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ); end; :: deftheorem Def5 defines order-generating WAYBEL_6:def_5_:_ for L being non empty RelStr for X being Subset of L holds ( X is order-generating iff for x being Element of L holds ( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) ); theorem Th15: :: WAYBEL_6:15 for L being lower-bounded up-complete LATTICE for X being Subset of L holds ( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) proofend; theorem :: WAYBEL_6:16 for L being lower-bounded up-complete LATTICE for X being Subset of L holds ( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds the carrier of L = Y ) proofend; theorem Th17: :: WAYBEL_6:17 for L being lower-bounded up-complete LATTICE for X being Subset of L holds ( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds ex p being Element of L st ( p in X & l1 <= p & not l2 <= p ) ) proofend; theorem Th18: :: WAYBEL_6:18 for L being lower-bounded continuous LATTICE for X being Subset of L st X = (IRR L) \ {(Top L)} holds X is order-generating proofend; theorem Th19: :: WAYBEL_6:19 for L being lower-bounded continuous LATTICE for X, Y being Subset of L st X is order-generating & X c= Y holds Y is order-generating proofend; begin definition let L be non empty RelStr ; let l be Element of L; attrl is prime means :Def6: :: WAYBEL_6:def 6 for x, y being Element of L holds ( not x "/\" y <= l or x <= l or y <= l ); end; :: deftheorem Def6 defines prime WAYBEL_6:def_6_:_ for L being non empty RelStr for l being Element of L holds ( l is prime iff for x, y being Element of L holds ( not x "/\" y <= l or x <= l or y <= l ) ); definition let L be non empty RelStr ; func PRIME L -> Subset of L means :Def7: :: WAYBEL_6:def 7 for x being Element of L holds ( x in it iff x is prime ); existence ex b1 being Subset of L st for x being Element of L holds ( x in b1 iff x is prime ) proofend; uniqueness for b1, b2 being Subset of L st ( for x being Element of L holds ( x in b1 iff x is prime ) ) & ( for x being Element of L holds ( x in b2 iff x is prime ) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines PRIME WAYBEL_6:def_7_:_ for L being non empty RelStr for b2 being Subset of L holds ( b2 = PRIME L iff for x being Element of L holds ( x in b2 iff x is prime ) ); definition let L be non empty RelStr ; let l be Element of L; attrl is co-prime means :Def8: :: WAYBEL_6:def 8 l ~ is prime ; end; :: deftheorem Def8 defines co-prime WAYBEL_6:def_8_:_ for L being non empty RelStr for l being Element of L holds ( l is co-prime iff l ~ is prime ); theorem Th20: :: WAYBEL_6:20 for L being non empty antisymmetric upper-bounded RelStr holds Top L is prime proofend; theorem :: WAYBEL_6:21 for L being non empty antisymmetric lower-bounded RelStr holds Bottom L is co-prime proofend; registration let L be non empty antisymmetric upper-bounded RelStr ; cluster prime for Element of the carrier of L; existence ex b1 being Element of L st b1 is prime proofend; end; theorem Th22: :: WAYBEL_6:22 for L being Semilattice for l being Element of L holds ( l is prime iff for A being non empty finite Subset of L st l >= inf A holds ex a being Element of L st ( a in A & l >= a ) ) proofend; theorem Th23: :: WAYBEL_6:23 for L being sup-Semilattice for x being Element of L holds ( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds ex a being Element of L st ( a in A & x <= a ) ) proofend; theorem Th24: :: WAYBEL_6:24 for L being LATTICE for l being Element of L st l is prime holds l is irreducible proofend; theorem Th25: :: WAYBEL_6:25 for L being LATTICE for l being Element of L holds ( l is prime iff for x being set for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds ( f . p = {} iff p <= l ) ) holds ( f is meet-preserving & f is join-preserving ) ) proofend; theorem Th26: :: WAYBEL_6:26 for L being upper-bounded LATTICE for l being Element of L st l <> Top L holds ( l is prime iff (downarrow l) ` is Filter of L ) proofend; theorem Th27: :: WAYBEL_6:27 for L being distributive LATTICE for l being Element of L holds ( l is prime iff l is irreducible ) proofend; theorem Th28: :: WAYBEL_6:28 for L being distributive LATTICE holds PRIME L = IRR L proofend; theorem :: WAYBEL_6:29 for L being Boolean LATTICE for l being Element of L st l <> Top L holds ( l is prime iff for x being Element of L st x > l holds x = Top L ) proofend; theorem :: WAYBEL_6:30 for L being lower-bounded distributive continuous LATTICE for l being Element of L st l <> Top L holds ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` ) proofend; theorem Th31: :: WAYBEL_6:31 for L being RelStr for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}}) proofend; theorem Th32: :: WAYBEL_6:32 for L being non empty RelStr for p, x being Element of L holds ( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p ) proofend; theorem Th33: :: WAYBEL_6:33 for L being upper-bounded LATTICE for f being Function of L,(BoolePoset {{}}) for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds ( f is meet-preserving & f is join-preserving ) proofend; theorem Th34: :: WAYBEL_6:34 for L being complete LATTICE st PRIME L is order-generating holds ( L is distributive & L is meet-continuous ) proofend; theorem Th35: :: WAYBEL_6:35 for L being lower-bounded continuous LATTICE holds ( L is distributive iff PRIME L is order-generating ) proofend; theorem :: WAYBEL_6:36 for L being lower-bounded continuous LATTICE holds ( L is distributive iff L is Heyting ) proofend; theorem Th37: :: WAYBEL_6:37 for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) holds for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) proofend; Lm2: for L being complete continuous LATTICE st ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) holds L is completely-distributive proofend; Lm3: for L being complete completely-distributive LATTICE holds ( L is distributive & L is continuous & L ~ is continuous ) proofend; Lm4: for L being complete LATTICE st L is distributive & L is continuous & L ~ is continuous holds for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) proofend; theorem :: WAYBEL_6:38 for L being complete LATTICE holds ( L is completely-distributive iff ( L is continuous & ( for l being Element of L ex X being Subset of L st ( l = sup X & ( for x being Element of L st x in X holds x is co-prime ) ) ) ) ) proofend; theorem :: WAYBEL_6:39 for L being complete LATTICE holds ( L is completely-distributive iff ( L is distributive & L is continuous & L opp is continuous ) ) proofend;