:: Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received March 4, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: WAYBEL13:1
theorem Th2: :: WAYBEL13:2
theorem Th3: :: WAYBEL13:3
theorem Th4: :: WAYBEL13:4
theorem Th5: :: WAYBEL13:5
theorem Th6: :: WAYBEL13:6
theorem Th7: :: WAYBEL13:7
theorem Th8: :: WAYBEL13:8
theorem Th9: :: WAYBEL13:9
theorem Th10: :: WAYBEL13:10
theorem Th11: :: WAYBEL13:11
theorem Th12: :: WAYBEL13:12
theorem :: WAYBEL13:13
theorem :: WAYBEL13:14
theorem Th15: :: WAYBEL13:15
theorem Th16: :: WAYBEL13:16
theorem :: WAYBEL13:17
theorem Th18: :: WAYBEL13:18
theorem Th19: :: WAYBEL13:19
theorem Th20: :: WAYBEL13:20
theorem Th21: :: WAYBEL13:21
theorem Th22: :: WAYBEL13:22
theorem Th23: :: WAYBEL13:23
theorem Th24: :: WAYBEL13:24
theorem :: WAYBEL13:25
Lm2:
for L being lower-bounded LATTICE st L is algebraic holds
ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
theorem Th26: :: WAYBEL13:26
Lm3:
for L being LATTICE st ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
Lm4:
for L being LATTICE st ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
Lm5:
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 st x << y holds
f . x << f . y
theorem Th27: :: WAYBEL13:27
theorem Th28: :: WAYBEL13:28
theorem Th29: :: WAYBEL13:29
theorem Th30: :: WAYBEL13:30
theorem Th31: :: WAYBEL13:31
theorem Th32: :: WAYBEL13:32
Lm6:
for L being LATTICE st ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) holds
L is algebraic
theorem :: WAYBEL13:33
theorem :: WAYBEL13:34
theorem :: WAYBEL13:35