:: Bases of Continuous Lattices
:: by Robert Milewski
::
:: Received November 28, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: WAYBEL23:1
Lm1:
for X being non empty set
for Y being Subset of (InclPoset X) st ex_sup_of Y, InclPoset X holds
union Y c= sup Y
theorem Th2: :: WAYBEL23:2
theorem Th3: :: WAYBEL23:3
theorem :: WAYBEL23:4
theorem Th5: :: WAYBEL23:5
theorem Th6: :: WAYBEL23:6
theorem Th7: :: WAYBEL23:7
theorem :: WAYBEL23:8
theorem :: WAYBEL23:9
theorem :: WAYBEL23:10
theorem Th11: :: WAYBEL23:11
theorem Th12: :: WAYBEL23:12
theorem :: WAYBEL23:13
theorem :: WAYBEL23:14
:: deftheorem Def1 defines meet-closed WAYBEL23:def 1 :
:: deftheorem Def2 defines join-closed WAYBEL23:def 2 :
:: deftheorem Def3 defines infs-closed WAYBEL23:def 3 :
:: deftheorem Def4 defines sups-closed WAYBEL23:def 4 :
theorem Th15: :: WAYBEL23:15
theorem Th16: :: WAYBEL23:16
theorem :: WAYBEL23:17
theorem Th18: :: WAYBEL23:18
theorem :: WAYBEL23:19
theorem :: WAYBEL23:20
theorem Th21: :: WAYBEL23:21
theorem Th22: :: WAYBEL23:22
theorem :: WAYBEL23:23
theorem :: WAYBEL23:24
theorem Th25: :: WAYBEL23:25
theorem Th26: :: WAYBEL23:26
theorem :: WAYBEL23:27
theorem :: WAYBEL23:28
theorem Th29: :: WAYBEL23:29
theorem Th30: :: WAYBEL23:30
theorem :: WAYBEL23:31
theorem :: WAYBEL23:32
theorem Th33: :: WAYBEL23:33
theorem :: WAYBEL23:34
theorem Th35: :: WAYBEL23:35
theorem Th36: :: WAYBEL23:36
theorem Th37: :: WAYBEL23:37
theorem Th38: :: WAYBEL23:38
theorem Th39: :: WAYBEL23:39
theorem Th40: :: WAYBEL23:40
theorem Th41: :: WAYBEL23:41
:: deftheorem defines weight WAYBEL23:def 5 :
:: deftheorem defines second-countable WAYBEL23:def 6 :
:: deftheorem Def7 defines CLbasis WAYBEL23:def 7 :
:: deftheorem Def8 defines with_bottom WAYBEL23:def 8 :
:: deftheorem Def9 defines with_top WAYBEL23:def 9 :
theorem Th42: :: WAYBEL23:42
theorem Th43: :: WAYBEL23:43
theorem Th44: :: WAYBEL23:44
theorem :: WAYBEL23:45
theorem Th46: :: WAYBEL23:46
theorem Th47: :: WAYBEL23:47
Lm2:
for L being lower-bounded continuous LATTICE
for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) holds
( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
Lm3:
for L being lower-bounded continuous LATTICE
for B being Subset of L st ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) holds
for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b << y )
theorem Th48: :: WAYBEL23:48
theorem :: WAYBEL23:49
theorem Th50: :: WAYBEL23:50
:: deftheorem Def10 defines supMap WAYBEL23:def 10 :
:: deftheorem Def11 defines idsMap WAYBEL23:def 11 :
:: deftheorem Def12 defines baseMap WAYBEL23:def 12 :
theorem Th51: :: WAYBEL23:51
theorem Th52: :: WAYBEL23:52
theorem Th53: :: WAYBEL23:53
theorem Th54: :: WAYBEL23:54
theorem Th55: :: WAYBEL23:55
theorem :: WAYBEL23:56
theorem :: WAYBEL23:57
theorem Th58: :: WAYBEL23:58
theorem Th59: :: WAYBEL23:59
theorem Th60: :: WAYBEL23:60
theorem Th61: :: WAYBEL23:61
theorem Th62: :: WAYBEL23:62
theorem Th63: :: WAYBEL23:63
theorem Th64: :: WAYBEL23:64
theorem Th65: :: WAYBEL23:65
theorem Th66: :: WAYBEL23:66
theorem Th67: :: WAYBEL23:67
theorem :: WAYBEL23:68
canceled;
theorem Th69: :: WAYBEL23:69
theorem :: WAYBEL23:70
Lm4:
for L being lower-bounded continuous LATTICE st L is algebraic holds
( the carrier of (CompactSublatt L) is with_bottom CLbasis of L & ( for B being with_bottom CLbasis of L holds the carrier of (CompactSublatt L) c= B ) )
theorem Th71: :: WAYBEL23:71
Lm5:
for L being lower-bounded continuous LATTICE st ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 holds
L is algebraic
theorem :: WAYBEL23:72
theorem :: WAYBEL23:73
theorem :: WAYBEL23:74
theorem :: WAYBEL23:75