:: On The Topological Properties of Meet-Continuous Lattices
:: by Artur Korni{\l}owicz
::
:: Received December 20, 1996
:: Copyright (c) 1996 Association of Mizar Users
:: deftheorem Def1 defines antitone WAYBEL_9:def 1 :
theorem Th1: :: WAYBEL_9:1
theorem Th2: :: WAYBEL_9:2
theorem :: WAYBEL_9:3
Lm1:
for L being reflexive antisymmetric with_infima RelStr
for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x }
theorem Th4: :: WAYBEL_9:4
Lm2:
for L being reflexive antisymmetric with_suprema RelStr
for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x }
theorem Th5: :: WAYBEL_9:5
theorem :: WAYBEL_9:6
theorem Th7: :: WAYBEL_9:7
theorem Th8: :: WAYBEL_9:8
Lm3:
for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of L
for n being Function of D,the carrier of L holds NetStr(# D,(the InternalRel of L |_2 D),n #) is net of L
theorem Th9: :: WAYBEL_9:9
theorem Th10: :: WAYBEL_9:10
:: deftheorem defines inf WAYBEL_9:def 2 :
:: deftheorem Def3 defines ex_sup_of WAYBEL_9:def 3 :
:: deftheorem Def4 defines ex_inf_of WAYBEL_9:def 4 :
:: deftheorem Def5 defines +id WAYBEL_9:def 5 :
:: deftheorem Def6 defines opp+id WAYBEL_9:def 6 :
theorem Th11: :: WAYBEL_9:11
:: deftheorem Def7 defines | WAYBEL_9:def 7 :
theorem :: WAYBEL_9:12
theorem Th13: :: WAYBEL_9:13
theorem Th14: :: WAYBEL_9:14
theorem :: WAYBEL_9:15
theorem Th16: :: WAYBEL_9:16
theorem Th17: :: WAYBEL_9:17
definition
let S be non
empty 1-sorted ;
let T be
1-sorted ;
let f be
Function of
S,
T;
let N be
NetStr of
S;
func f * N -> strict NetStr of
T means :
Def8:
:: WAYBEL_9:def 8
(
RelStr(# the
carrier of
it,the
InternalRel of
it #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #) & the
mapping of
it = f * the
mapping of
N );
existence
ex b1 being strict NetStr of T st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = f * the mapping of N )
uniqueness
for b1, b2 being strict NetStr of T st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = f * the mapping of N & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b2 = f * the mapping of N holds
b1 = b2
;
end;
:: deftheorem Def8 defines * WAYBEL_9:def 8 :
theorem Th18: :: WAYBEL_9:18
theorem :: WAYBEL_9:19
theorem :: WAYBEL_9:20
Lm4:
for tau being Subset-Family of {0 }
for r being Relation of {0 } st tau = {{} ,{0 }} & r = {[0 ,0 ]} holds
( TopRelStr(# {0 },r,tau #) is trivial & TopRelStr(# {0 },r,tau #) is reflexive & not TopRelStr(# {0 },r,tau #) is empty & TopRelStr(# {0 },r,tau #) is discrete & TopRelStr(# {0 },r,tau #) is finite )
theorem Th21: :: WAYBEL_9:21
theorem Th22: :: WAYBEL_9:22
theorem :: WAYBEL_9:23
theorem Th24: :: WAYBEL_9:24
theorem Th25: :: WAYBEL_9:25
theorem Th26: :: WAYBEL_9:26
theorem Th27: :: WAYBEL_9:27
theorem Th28: :: WAYBEL_9:28
:: deftheorem Def9 defines is_a_cluster_point_of WAYBEL_9:def 9 :
theorem :: WAYBEL_9:29
theorem Th30: :: WAYBEL_9:30
theorem Th31: :: WAYBEL_9:31
theorem Th32: :: WAYBEL_9:32
theorem Th33: :: WAYBEL_9:33
theorem Th34: :: WAYBEL_9:34
Lm5:
for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-directed & c is_a_cluster_point_of N holds
d is_>=_than rng the mapping of N
Lm6:
for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_<=_than b holds
d <= b
theorem Th35: :: WAYBEL_9:35
Lm7:
for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & N is eventually-filtered & c is_a_cluster_point_of N holds
d is_<=_than rng the mapping of N
Lm8:
for S being Hausdorff compact TopLattice
for N being net of S
for c being Point of S
for d being Element of S st c = d & ( for x being Element of S holds x "/\" is continuous ) & c is_a_cluster_point_of N holds
for b being Element of S st rng the mapping of N is_>=_than b holds
d >= b
theorem Th36: :: WAYBEL_9:36
theorem Th37: :: WAYBEL_9:37
theorem Th38: :: WAYBEL_9:38
theorem Th39: :: WAYBEL_9:39
theorem :: WAYBEL_9:40
theorem :: WAYBEL_9:41