:: Introduction to Meet-Continuous Topological Lattices
:: by Artur Korni{\l}owicz
::
:: Received November 3, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: YELLOW13:1
theorem Th2: :: YELLOW13:2
theorem Th3: :: YELLOW13:3
theorem Th4: :: YELLOW13:4
theorem Th5: :: YELLOW13:5
theorem Th6: :: YELLOW13:6
theorem :: YELLOW13:7
theorem Th8: :: YELLOW13:8
theorem Th9: :: YELLOW13:9
theorem :: YELLOW13:10
theorem Th11: :: YELLOW13:11
theorem Th12: :: YELLOW13:12
theorem :: YELLOW13:13
theorem :: YELLOW13:14
theorem :: YELLOW13:15
Lm1:
for T being non empty TopStruct
for A being Subset of T
for p being Point of T st p in Cl A holds
for K being Basis of p
for Q being Subset of T st Q in K holds
A meets Q
Lm2:
for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ( for K being Basis of p
for Q being Subset of T st Q in K holds
A meets Q ) holds
ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q
Lm3:
for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ex K being Basis of p st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A
theorem :: YELLOW13:16
theorem :: YELLOW13:17
:: deftheorem Def1 defines basis YELLOW13:def 1 :
:: deftheorem defines basis YELLOW13:def 2 :
theorem Th18: :: YELLOW13:18
theorem Th19: :: YELLOW13:19
:: deftheorem Def3 defines correct YELLOW13:def 3 :
theorem :: YELLOW13:20
theorem :: YELLOW13:21
theorem :: YELLOW13:22
theorem :: YELLOW13:23
:: deftheorem Def4 defines basis YELLOW13:def 4 :
theorem Th24: :: YELLOW13:24
theorem Th25: :: YELLOW13:25
theorem :: YELLOW13:26
theorem :: YELLOW13:27
:: deftheorem Def5 defines topological_semilattice YELLOW13:def 5 :
theorem Th28: :: YELLOW13:28