Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Algebraic and Arithmetic Lattices. Part II

**by****Robert Milewski**- Received October 29, 1997
- MML identifier: WAYBEL15

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, CAT_1, YELLOW_0, WELLORD1, PRE_TOPC, SGRAPH1, FUNCT_1, RELAT_1, YELLOW_1, WAYBEL_0, LATTICES, RELAT_2, WAYBEL_1, GROUP_6, SEQM_3, WAYBEL_8, COMPTS_1, FINSET_1, BOOLE, LATTICE3, QUANTAL1, WAYBEL_3, ORDINAL2, YELLOW_2, FILTER_2, BINOP_1, BHSP_3, WAYBEL_6, OPPCAT_1, FILTER_0, ZF_LANG, WAYBEL_5, WAYBEL15; notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, WELLORD1, FUNCT_1, FUNCT_2, FINSET_1, STRUCT_0, ORDERS_1, PRE_TOPC, QUANTAL1, GRCAT_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8; constructors ORDERS_3, TOLER_1, QUANTAL1, TOPS_2, GRCAT_1, YELLOW_3, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8; clusters STRUCT_0, RELSET_1, FINSET_1, FUNCT_1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries theorem :: WAYBEL15:1 for R be RelStr for S be full SubRelStr of R for T be full SubRelStr of S holds T is full SubRelStr of R; theorem :: WAYBEL15:2 for X be 1-sorted, Y,Z be non empty 1-sorted for f be map of X,Y for g be map of Y,Z holds f is onto & g is onto implies g*f is onto; theorem :: WAYBEL15:3 for X be 1-sorted for Y be Subset of X holds (id X).:Y = Y; theorem :: WAYBEL15:4 for X be set for a be Element of BoolePoset X holds uparrow a = {Y where Y is Subset of X : a c= Y}; theorem :: WAYBEL15:5 for L be upper-bounded non empty antisymmetric RelStr for a be Element of L holds Top L <= a implies a = Top L; theorem :: WAYBEL15:6 for S,T be non empty Poset for g be map of S,T for d be map of T,S holds g is onto & [g,d] is Galois implies T,Image d are_isomorphic; theorem :: WAYBEL15:7 for L1,L2,L3 be non empty Poset for g1 be map of L1,L2 for g2 be map of L2,L3 for d1 be map of L2,L1 for d2 be map of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds [g2*g1,d1*d2] is Galois; theorem :: WAYBEL15:8 for L1,L2 be non empty Poset for f be map of L1,L2 for f1 be map of L2,L1 st f1 = (f qua Function)" & f is isomorphic holds [f,f1] is Galois & [f1,f] is Galois; theorem :: WAYBEL15:9 for X be set holds BoolePoset X is arithmetic; definition let X be set; cluster BoolePoset X -> arithmetic; end; theorem :: WAYBEL15:10 for L1,L2 be up-complete (non empty Poset) for f be map of L1,L2 st f is isomorphic for x be Element of L1 holds f.:(waybelow x) = waybelow f.x; theorem :: WAYBEL15:11 for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is continuous holds L2 is continuous; theorem :: WAYBEL15:12 for L1,L2 be LATTICE st L1,L2 are_isomorphic & L1 is lower-bounded arithmetic holds L2 is arithmetic; theorem :: WAYBEL15:13 for L1,L2,L3 be non empty Poset for f be map of L1,L2 for g be map of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds g*f is directed-sups-preserving; begin :: Maps Preserving Sup's and Inf's theorem :: WAYBEL15:14 for L1,L2 be non empty RelStr for f be map of L1,L2 for X be Subset of Image f holds (inclusion f).:X = X; theorem :: WAYBEL15:15 for X be set for c be map of BoolePoset X,BoolePoset X st c is idempotent directed-sups-preserving holds inclusion c is directed-sups-preserving; theorem :: WAYBEL15:16 :: THEOREM 2.10. for L be continuous complete LATTICE for p be kernel map of L,L st p is directed-sups-preserving holds Image p is continuous LATTICE; theorem :: WAYBEL15:17 :: THEOREM 2.14. for L be continuous complete LATTICE for p be projection map of L,L st p is directed-sups-preserving holds Image p is continuous LATTICE; theorem :: WAYBEL15:18 :: THEOREM 4.16. (1) iff (2) for L be lower-bounded LATTICE holds L is continuous iff ex A be arithmetic lower-bounded LATTICE, g be map of A,L st g is onto & g is infs-preserving & g is directed-sups-preserving; theorem :: WAYBEL15:19 :: THEOREM 4.16. (1) iff (3) for L be lower-bounded LATTICE holds L is continuous iff ex A be algebraic lower-bounded LATTICE, g be map of A,L st g is onto & g is infs-preserving & g is directed-sups-preserving; theorem :: WAYBEL15:20 :: THEOREM 4.16. (1) iff (4) for L be lower-bounded LATTICE holds ( L is continuous implies ex X be non empty set, p be projection map of BoolePoset X,BoolePoset X st p is directed-sups-preserving & L,Image p are_isomorphic ) & (( ex X be set, p be projection map of BoolePoset X,BoolePoset X st p is directed-sups-preserving & L,Image p are_isomorphic ) implies L is continuous ); begin :: Atoms Elements theorem :: WAYBEL15:21 for L be non empty RelStr for x be Element of L holds x in PRIME (L opp) iff x is co-prime; definition let L be non empty RelStr; let a be Element of L; attr a is atom means :: WAYBEL15:def 1 Bottom L < a & for b be Element of L st Bottom L < b & b <= a holds b = a; end; definition let L be non empty RelStr; func ATOM L -> Subset of L means :: WAYBEL15:def 2 for x be Element of L holds x in it iff x is atom; end; canceled; theorem :: WAYBEL15:23 for L be Boolean LATTICE for a be Element of L holds a is atom iff a is co-prime & a <> Bottom L; definition let L be Boolean LATTICE; cluster atom -> co-prime Element of L; end; theorem :: WAYBEL15:24 for L be Boolean LATTICE holds ATOM L = (PRIME (L opp)) \ {Bottom L}; theorem :: WAYBEL15:25 for L be Boolean LATTICE for x,a be Element of L st a is atom holds a <= x iff not a <= 'not' x; theorem :: WAYBEL15:26 for L be complete Boolean LATTICE for X be Subset of L for x be Element of L holds x "/\" sup X = "\/"({x"/\"y where y is Element of L: y in X},L); theorem :: WAYBEL15:27 for L be lower-bounded with_infima antisymmetric non empty RelStr for x,y be Element of L st x is atom & y is atom & x <> y holds x "/\" y = Bottom L; theorem :: WAYBEL15:28 for L be complete Boolean LATTICE for x be Element of L for A be Subset of L st A c= ATOM L holds x in A iff x is atom & x <= sup A; theorem :: WAYBEL15:29 for L be complete Boolean LATTICE for X,Y be Subset of L st X c= ATOM L & Y c= ATOM L holds X c= Y iff sup X <= sup Y; begin :: More on the Boolean Lattice theorem :: WAYBEL15:30 :: THEOREM 4.18. (2) iff (1) for L be Boolean LATTICE holds L is arithmetic iff ex X be set st L,BoolePoset X are_isomorphic; theorem :: WAYBEL15:31 :: THEOREM 4.18. (2) iff (3) for L be Boolean LATTICE holds L is arithmetic iff L is algebraic; theorem :: WAYBEL15:32 :: THEOREM 4.18. (2) iff (4) for L be Boolean LATTICE holds L is arithmetic iff L is continuous; theorem :: WAYBEL15:33 :: THEOREM 4.18. (2) iff (5) for L be Boolean LATTICE holds L is arithmetic iff (L is continuous & L opp is continuous); theorem :: WAYBEL15:34 :: THEOREM 4.18. (2) iff (6) for L be Boolean LATTICE holds L is arithmetic iff L is completely-distributive; theorem :: WAYBEL15:35 :: THEOREM 4.18. (2) iff (7) for L be Boolean LATTICE holds L is arithmetic iff ( L is complete & for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X );

Back to top