Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Algebraic and Arithmetic Lattices. Part I

**by****Robert Milewski**- Received March 4, 1997
- MML identifier: WAYBEL13

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, RELAT_2, ORDERS_1, WAYBEL_8, COMPTS_1, YELLOW_0, LATTICE3, FILTER_2, SUBSET_1, LATTICES, WAYBEL_0, WAYBEL_5, GROUP_6, WAYBEL10, YELLOW_1, FINSET_1, SETFAM_1, BHSP_3, BOOLE, CAT_1, WELLORD2, QUANTAL1, TARSKI, ORDINAL2, PRE_TOPC, WAYBEL_3, SEQM_3, PBOOLE, CARD_3, WELLORD1, WAYBEL_1, YELLOW_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, STRUCT_0, RELAT_1, ORDERS_1, FUNCT_1, FUNCT_2, PRE_TOPC, PBOOLE, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10, GRCAT_1; constructors DOMAIN_1, QUANTAL1, ORDERS_3, YELLOW_3, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL10, GRCAT_1; clusters STRUCT_0, FINSET_1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL10, RELSET_1, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries scheme LambdaCD{A()->non empty set,C[set],F(set)->set,G(set)->set}: ex f being Function st dom f = A() & for x be Element of A() holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)); theorem :: WAYBEL13:1 for L be non empty reflexive transitive RelStr for x,y be Element of L holds x <= y implies compactbelow x c= compactbelow y; theorem :: WAYBEL13:2 for L be non empty reflexive RelStr for x be Element of L holds compactbelow x is Subset of CompactSublatt L; theorem :: WAYBEL13:3 for L be RelStr for S be SubRelStr of L for X be Subset of S holds X is Subset of L; theorem :: WAYBEL13:4 for L be with_suprema non empty reflexive transitive RelStr holds the carrier of L is Ideal of L; theorem :: WAYBEL13:5 for L1 be lower-bounded non empty reflexive antisymmetric RelStr for L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the RelStr of L2 & L1 is up-complete holds the carrier of CompactSublatt L1 = the carrier of CompactSublatt L2; begin :: Algebraic and Arithmetic Lattices theorem :: WAYBEL13:6 :: COROLLARY 4.10. for L be algebraic lower-bounded LATTICE for S be CLSubFrame of L holds S is algebraic; theorem :: WAYBEL13:7 :: EXAMPLES 4.11.(2) for X,E be set for L be CLSubFrame of BoolePoset X holds E in the carrier of CompactSublatt L iff ( ex F be Element of BoolePoset X st F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ); theorem :: WAYBEL13:8 for L be lower-bounded sup-Semilattice holds InclPoset Ids L is CLSubFrame of BoolePoset the carrier of L; definition let L be non empty reflexive transitive RelStr; cluster principal Ideal of L; end; theorem :: WAYBEL13:9 for L be lower-bounded sup-Semilattice for X be non empty directed Subset of InclPoset Ids L holds sup X = union X; theorem :: WAYBEL13:10 :: PROPOSITION 4.12.(i) for S be lower-bounded sup-Semilattice holds InclPoset Ids S is algebraic; theorem :: WAYBEL13:11 :: PROPOSITION 4.12.(i) for S be lower-bounded sup-Semilattice for x be Element of InclPoset Ids S holds x is compact iff x is principal Ideal of S; theorem :: WAYBEL13:12 for S be lower-bounded sup-Semilattice for x be Element of InclPoset Ids S holds x is compact iff ex a be Element of S st x = downarrow a; theorem :: WAYBEL13:13 :: PROPOSITION 4.12.(ii) for L be lower-bounded sup-Semilattice for f be map of L, CompactSublatt InclPoset Ids L st for x be Element of L holds f.x = downarrow x holds f is isomorphic; theorem :: WAYBEL13:14 :: PROPOSITION 4.12.(iii) for S be lower-bounded LATTICE holds InclPoset Ids S is arithmetic; theorem :: WAYBEL13:15 :: PROPOSITION 4.12.(iv) for L be lower-bounded sup-Semilattice holds CompactSublatt L is lower-bounded sup-Semilattice; theorem :: WAYBEL13:16 :: PROPOSITION 4.12.(v) for L be algebraic lower-bounded sup-Semilattice for f be map of L,InclPoset Ids CompactSublatt L st for x be Element of L holds f.x = compactbelow x holds f is isomorphic; theorem :: WAYBEL13:17 :: PROPOSITION 4.12.(vi) for L be algebraic lower-bounded sup-Semilattice for x be Element of L holds compactbelow x is principal Ideal of CompactSublatt L iff x is compact; begin :: Maps theorem :: WAYBEL13:18 for L1,L2 be non empty RelStr for X be Subset of L1, x be Element of L1 for f be map of L1,L2 st f is isomorphic holds x is_<=_than X iff f.x is_<=_than f.:X; theorem :: WAYBEL13:19 for L1,L2 be non empty RelStr for X be Subset of L1, x be Element of L1 for f be map of L1,L2 st f is isomorphic holds x is_>=_than X iff f.x is_>=_than f.:X; theorem :: WAYBEL13:20 for L1,L2 be non empty antisymmetric RelStr for f be map of L1,L2 holds f is isomorphic implies f is infs-preserving sups-preserving; definition let L1,L2 be non empty antisymmetric RelStr; cluster isomorphic -> infs-preserving sups-preserving map of L1,L2; end; theorem :: WAYBEL13:21 for L1,L2,L3 be non empty transitive antisymmetric RelStr for f be map of L1,L2 st f is infs-preserving holds L2 is full infs-inheriting SubRelStr of L3 & L3 is complete implies ex g be map of L1,L3 st f = g & g is infs-preserving; theorem :: WAYBEL13:22 for L1,L2,L3 be non empty transitive antisymmetric RelStr for f be map of L1,L2 st f is monotone directed-sups-preserving holds L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g be map of L1,L3 st f = g & g is directed-sups-preserving; theorem :: WAYBEL13:23 for L be lower-bounded sup-Semilattice holds InclPoset Ids CompactSublatt L is CLSubFrame of BoolePoset the carrier of CompactSublatt L; theorem :: WAYBEL13:24 :: COROLLARY 4.13. for L be algebraic lower-bounded LATTICE ex g be map of L,BoolePoset the carrier of CompactSublatt L st g is infs-preserving & g is directed-sups-preserving & g is one-to-one & for x be Element of L holds g.x = compactbelow x; theorem :: WAYBEL13:25 :: PROPOSITION 4.14. for I be non empty set for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds J.i is algebraic lower-bounded LATTICE holds product J is algebraic lower-bounded LATTICE; theorem :: WAYBEL13:26 for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 holds L1,L2 are_isomorphic; theorem :: WAYBEL13:27 for L1,L2 be up-complete (non empty Poset) for f be map of L1,L2 st f is isomorphic for x,y be Element of L1 holds x << y iff f.x << f.y; theorem :: WAYBEL13:28 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 x is compact iff f.x is compact; theorem :: WAYBEL13:29 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.:(compactbelow x) = compactbelow f.x; theorem :: WAYBEL13:30 for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is up-complete holds L2 is up-complete; theorem :: WAYBEL13:31 for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is complete satisfying_axiom_K holds L2 is satisfying_axiom_K; theorem :: WAYBEL13:32 for L1,L2 be sup-Semilattice st L1,L2 are_isomorphic & L1 is lower-bounded algebraic holds L2 is algebraic; theorem :: WAYBEL13:33 for L be continuous lower-bounded sup-Semilattice holds SupMap L is infs-preserving sups-preserving; theorem :: WAYBEL13:34 :: THEOREM 4.15. (1) iff (2) for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be non empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) & (( ex X be set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ); theorem :: WAYBEL13:35 :: THEOREM 4.15. (1) iff (3) for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be non empty set, c be closure map of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic ) & (( ex X be set, c be closure map of BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic ) implies L is algebraic );

Back to top