environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, RELAT_1, SEQM_3, FUNCT_1, WAYBEL_0, SUBSET_1, XXREAL_0, STRUCT_0, SETFAM_1, RELAT_2, LATTICE3, LATTICES, TARSKI, EQREL_1, WELLORD1, YELLOW_0, CAT_1, ORDINAL2, WAYBEL_2, YELLOW_2, FINSUB_1, WELLORD2, YELLOW_1, YELLOW_6, PRE_TOPC, RCOMP_1, ZFMISC_1, ORDERS_1, CARD_1, NATTRA_1, FINSET_1, COMPTS_1, CONNSP_2, ORDINAL1, TOPS_1, SEQ_2, WAYBEL_7, MCART_1, XXREAL_2, WAYBEL_9;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1, FINSUB_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FINSET_1, SETFAM_1, TOLER_1, PARTFUN1, FUNCT_2, CARD_1, ORDINAL1, NUMBERS, ORDERS_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, ORDERS_2, COMPTS_1, CONNSP_2, LATTICE3, ORDERS_3, TDLAT_3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_4, WAYBEL_2, YELLOW_6;
definitions TARSKI, YELLOW_6, ORDERS_2, WAYBEL_0, WAYBEL_1, YELLOW_0, PRE_TOPC, WAYBEL_2, LATTICE3, TOPS_2, STRUCT_0, XBOOLE_0, FINSET_1;
theorems BORSUK_1, COMPTS_1, CONNSP_2, FINSET_1, FUNCT_1, FUNCT_2, ORDERS_2, ORDERS_1, PCOMPS_1, PRE_TOPC, RELAT_1, SETFAM_1, TARSKI, TOPS_1, WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4, YELLOW_6, YELLOW_7, ZFMISC_1, RELSET_1, TDLAT_3, WAYBEL_8, XBOOLE_0, XBOOLE_1, RELAT_2;
schemes YELLOW_0, FUNCT_2, XBOOLE_0;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSUB_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0, TDLAT_3, WAYBEL_0, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_6, COMPTS_1, TOPS_1, CARD_1, XTUPLE_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FINSUB_1, TOLER_1, TOPS_1, TOPS_2, CONNSP_2, PCOMPS_1, TDLAT_3, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, YELLOW_6, COMPTS_1, RELSET_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities WAYBEL_0, WAYBEL_2, LATTICE3, STRUCT_0, XBOOLE_0, WELLORD1;
expansions TARSKI, YELLOW_6, ORDERS_2, WAYBEL_0, PRE_TOPC, LATTICE3, TOPS_2, STRUCT_0, XBOOLE_0;
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 }
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 }
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
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 reflexive & TopRelStr(# {0},r,tau #) is discrete & TopRelStr(# {0},r,tau #) is finite & TopRelStr(# {0},r,tau #) is 1 -element )
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
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
:: Acknowledgements:
:: =================
::
:: I would like to thank Professor A. Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------