:: More on the Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received October 29, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: WAYBEL15:1
theorem Th2: :: WAYBEL15:2
theorem :: WAYBEL15:3
canceled;
theorem :: WAYBEL15:4
theorem :: WAYBEL15:5
theorem Th6: :: WAYBEL15:6
theorem Th7: :: WAYBEL15:7
theorem Th8: :: WAYBEL15:8
theorem Th9: :: WAYBEL15:9
theorem Th10: :: WAYBEL15:10
theorem Th11: :: WAYBEL15:11
theorem Th12: :: WAYBEL15:12
Lm2:
for L being lower-bounded LATTICE st L is continuous holds
ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
theorem Th13: :: WAYBEL15:13
theorem :: WAYBEL15:14
theorem Th15: :: WAYBEL15:15
Lm3:
for L being lower-bounded LATTICE st ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) holds
ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
theorem Th16: :: WAYBEL15:16
theorem Th17: :: WAYBEL15:17
Lm4:
for L being LATTICE st ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) holds
L is continuous
theorem :: WAYBEL15:18
theorem :: WAYBEL15:19
theorem :: WAYBEL15:20
theorem :: WAYBEL15:21
:: deftheorem Def1 defines atom WAYBEL15:def 1 :
:: deftheorem Def2 defines ATOM WAYBEL15:def 2 :
theorem :: WAYBEL15:22
canceled;
theorem Th23: :: WAYBEL15:23
theorem :: WAYBEL15:24
theorem :: WAYBEL15:25
theorem Th26: :: WAYBEL15:26
theorem Th27: :: WAYBEL15:27
theorem Th28: :: WAYBEL15:28
theorem Th29: :: WAYBEL15:29
Lm6:
for L being Boolean LATTICE st L is completely-distributive holds
( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) )
Lm7:
for L being Boolean LATTICE st L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) holds
ex Y being set st L, BoolePoset Y are_isomorphic
theorem :: WAYBEL15:30
theorem :: WAYBEL15:31
theorem :: WAYBEL15:32
theorem :: WAYBEL15:33
theorem :: WAYBEL15:34
theorem :: WAYBEL15:35