:: On The Topological Properties of Meet-Continuous Lattices :: by Artur Korni{\l}owicz :: :: Received December 20, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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 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; constructors 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; 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; requirements BOOLE, SUBSET; begin :: Preliminaries ::------------------------------------------------------------------- :: Acknowledgements: :: ================= :: :: I would like to thank Professor A. Trybulec for his help in the preparation :: of the article. ::------------------------------------------------------------------- registration let L be non empty RelStr; cluster id L -> monotone; end; definition let S, T be non empty RelStr, f be Function of S,T; redefine attr f is antitone means :: WAYBEL_9:def 1 for x, y being Element of S st x <= y holds f.x >= f.y; end; theorem :: WAYBEL_9:1 for S, T being RelStr, K, L being non empty RelStr for f being Function of S, T, g being Function of K, L st the RelStr of S = the RelStr of K & the RelStr of T = the RelStr of L & f = g & f is monotone holds g is monotone ; theorem :: WAYBEL_9:2 for S, T being RelStr, K, L being non empty RelStr for f being Function of S, T, g being Function of K, L st the RelStr of S = the RelStr of K & the RelStr of T = the RelStr of L & f = g & f is antitone holds g is antitone ; theorem :: WAYBEL_9:3 for A, B being 1-sorted for F being Subset-Family of A, G being Subset-Family of B st the carrier of A = the carrier of B & F = G & F is Cover of A holds G is Cover of B; theorem :: WAYBEL_9:4 for L being antisymmetric reflexive with_suprema RelStr, x being Element of L holds uparrow x = {x} "\/" [#]L; theorem :: WAYBEL_9:5 for L being antisymmetric reflexive with_infima RelStr, x being Element of L holds downarrow x = {x} "/\" [#]L; theorem :: WAYBEL_9:6 for L being antisymmetric reflexive with_infima RelStr, y being Element of L holds (y"/\").:(uparrow y) = {y}; theorem :: WAYBEL_9:7 for L being antisymmetric reflexive with_infima RelStr, x being Element of L holds (x"/\")"{x} = uparrow x; theorem :: WAYBEL_9:8 for T being non empty 1-sorted, N being non empty NetStr over T holds N is_eventually_in rng the mapping of N; registration let L be non empty reflexive RelStr, D be non empty directed Subset of L, n be Function of D, the carrier of L; cluster NetStr (#D,(the InternalRel of L)|_2 D,n#) -> directed; end; registration let L be non empty reflexive transitive RelStr, D be non empty directed Subset of L, n be Function of D, the carrier of L; cluster NetStr (#D,(the InternalRel of L)|_2 D,n#) -> transitive; end; :: cf WAYBEL_2:42 theorem :: WAYBEL_9:9 for L being non empty reflexive transitive RelStr st for x being Element of L, N being net of L st N is eventually-directed holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds L is satisfying_MC; theorem :: WAYBEL_9:10 for L being non empty RelStr, a being Element of L, N being net of L holds a "/\" N is net of L; registration let L be non empty RelStr, x be Element of L, N be net of L; cluster x "/\" N -> transitive; end; registration let L be non empty RelStr, x be Element of L, N be non empty reflexive NetStr over L; cluster x "/\" N -> reflexive; end; registration let L be non empty RelStr, x be Element of L, N be non empty antisymmetric NetStr over L; cluster x "/\" N -> antisymmetric; end; registration let L be non empty RelStr, x be Element of L, N be non empty transitive NetStr over L; cluster x "/\" N -> transitive; end; registration let L be non empty RelStr, J be set, f be Function of J,the carrier of L; cluster FinSups f -> transitive; end; begin :: The Operations Defined on Nets definition let L be non empty RelStr, N be NetStr over L; func inf N -> Element of L equals :: WAYBEL_9:def 2 Inf the mapping of N; end; definition let L be RelStr, N be NetStr over L; pred ex_sup_of N means :: WAYBEL_9:def 3 ex_sup_of rng the mapping of N,L; pred ex_inf_of N means :: WAYBEL_9:def 4 ex_inf_of rng the mapping of N,L; end; definition let L be RelStr; func L+id -> strict NetStr over L means :: WAYBEL_9:def 5 the RelStr of it = the RelStr of L & the mapping of it = id L; end; registration let L be non empty RelStr; cluster L+id -> non empty; end; registration let L be reflexive RelStr; cluster L+id -> reflexive; end; registration let L be antisymmetric RelStr; cluster L+id -> antisymmetric; end; registration let L be transitive RelStr; cluster L+id -> transitive; end; registration let L be with_suprema RelStr; cluster L+id -> directed; end; registration let L be directed RelStr; cluster L+id -> directed; end; registration let L be non empty RelStr; cluster L+id -> monotone eventually-directed; end; definition let L be RelStr; func L opp+id -> strict NetStr over L means :: WAYBEL_9:def 6 the carrier of it = the carrier of L & the InternalRel of it = (the InternalRel of L)~ & the mapping of it = id L; end; theorem :: WAYBEL_9:11 for L being RelStr holds the RelStr of L~ = the RelStr of L opp+id; registration let L be non empty RelStr; cluster L opp+id -> non empty; end; registration let L be reflexive RelStr; cluster L opp+id -> reflexive; end; registration let L be antisymmetric RelStr; cluster L opp+id -> antisymmetric; end; registration let L be transitive RelStr; cluster L opp+id -> transitive; end; registration let L be with_infima RelStr; cluster L opp+id -> directed; end; registration let L be non empty RelStr; cluster L opp+id -> antitone eventually-filtered; end; definition let L be non empty 1-sorted, N be non empty NetStr over L, i be Element of N; func N|i -> strict NetStr over L means :: WAYBEL_9:def 7 (for x being object holds x in the carrier of it iff ex y being Element of N st y = x & i <= y) & the InternalRel of it = (the InternalRel of N)|_2 the carrier of it & the mapping of it = (the mapping of N)|the carrier of it; end; theorem :: WAYBEL_9:12 for L being non empty 1-sorted, N being non empty NetStr over L for i being Element of N holds the carrier of N|i = { y where y is Element of N : i <= y }; theorem :: WAYBEL_9:13 for L being non empty 1-sorted, N being non empty NetStr over L for i being Element of N holds the carrier of N|i c= the carrier of N; theorem :: WAYBEL_9:14 for L being non empty 1-sorted, N being non empty NetStr over L for i being Element of N holds N|i is full SubNetStr of N; registration let L be non empty 1-sorted, N be non empty reflexive NetStr over L, i be Element of N; cluster N|i -> non empty reflexive; end; registration let L be non empty 1-sorted, N be non empty directed NetStr over L, i be Element of N; cluster N|i -> non empty; end; registration let L be non empty 1-sorted, N be non empty reflexive antisymmetric NetStr over L, i be Element of N; cluster N|i -> antisymmetric; end; registration let L be non empty 1-sorted, N be non empty directed antisymmetric NetStr over L, i be Element of N; cluster N|i -> antisymmetric; end; registration let L be non empty 1-sorted, N be non empty reflexive transitive NetStr over L, i be Element of N; cluster N|i -> transitive; end; registration let L be non empty 1-sorted, N be net of L, i be Element of N; cluster N|i -> transitive directed; end; theorem :: WAYBEL_9:15 for L being non empty 1-sorted, N being non empty reflexive NetStr over L for i, x being Element of N, x1 being Element of N|i st x = x1 holds N.x = (N|i).x1; theorem :: WAYBEL_9:16 for L being non empty 1-sorted, N being non empty directed NetStr over L for i, x being Element of N, x1 being Element of N|i st x = x1 holds N.x = (N|i).x1; theorem :: WAYBEL_9:17 for L being non empty 1-sorted, N being net of L, i being Element of N holds N|i is subnet of N; registration let T be non empty 1-sorted, N be net of T; cluster strict for subnet of N; end; definition let L be non empty 1-sorted, N be net of L, i be Element of N; redefine func N|i -> strict subnet of N; end; definition let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be NetStr over S; func f * N -> strict NetStr over T means :: WAYBEL_9:def 8 the RelStr of it = the RelStr of N & the mapping of it = f * the mapping of N; end; registration let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be non empty NetStr over S; cluster f * N -> non empty; end; registration let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be reflexive NetStr over S; cluster f * N -> reflexive; end; registration let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be antisymmetric NetStr over S; cluster f * N -> antisymmetric; end; registration let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be transitive NetStr over S; cluster f * N -> transitive; end; registration let S be non empty 1-sorted, T be 1-sorted, f be Function of S, T, N be directed NetStr over S; cluster f * N -> directed; end; theorem :: WAYBEL_9:18 for L being non empty RelStr, N being non empty NetStr over L for x being Element of L holds (x"/\")*N = x "/\" N; begin :: The Properties of Topological Spaces theorem :: WAYBEL_9:19 for S, T being TopStruct for F being Subset-Family of S, G being Subset-Family of T st the TopStruct of S = the TopStruct of T & F = G & F is open holds G is open; theorem :: WAYBEL_9:20 for S, T being TopStruct for F being Subset-Family of S, G being Subset-Family of T st the TopStruct of S = the TopStruct of T & F = G & F is closed holds G is closed; definition struct(TopStruct,RelStr) TopRelStr (# carrier -> set, InternalRel -> ( Relation of the carrier), topology -> Subset-Family of the carrier #); end; registration let A be non empty set, R be Relation of A,A, T be Subset-Family of A; cluster TopRelStr (#A,R,T#) -> non empty; end; registration let x be set, R be Relation of {x}; let T be Subset-Family of {x}; cluster TopRelStr (#{x}, R, T#) -> 1-element; end; registration let X be set, O be Order of X, T be Subset-Family of X; cluster TopRelStr (#X, O, T#) -> reflexive transitive antisymmetric; end; registration cluster reflexive discrete strict finite 1-element for TopRelStr; end; definition mode TopLattice is with_infima with_suprema reflexive transitive antisymmetric TopSpace-like TopRelStr; end; registration cluster strict discrete finite compact Hausdorff 1-element for TopLattice; end; registration let T be Hausdorff non empty TopSpace; cluster -> Hausdorff for non empty SubSpace of T; end; theorem :: WAYBEL_9:21 for T being non empty TopSpace, p being Point of T for A being Element of OpenNeighborhoods p holds A is a_neighborhood of p; theorem :: WAYBEL_9:22 for T being non empty TopSpace, p being Point of T for A, B being Element of OpenNeighborhoods p holds A /\ B is Element of OpenNeighborhoods p; theorem :: WAYBEL_9:23 for T being non empty TopSpace, p being Point of T for A, B being Element of OpenNeighborhoods p holds A \/ B is Element of OpenNeighborhoods p ; theorem :: WAYBEL_9:24 for T being non empty TopSpace, p being Element of T for N being net of T st p in Lim N for S being Subset of T st S = rng the mapping of N holds p in Cl S; theorem :: WAYBEL_9:25 for T being Hausdorff TopLattice, N being convergent net of T for f being Function of T, T st f is continuous holds f.(lim N) in Lim (f * N); theorem :: WAYBEL_9:26 for T being Hausdorff TopLattice, N being convergent net of T for x being Element of T st x"/\" is continuous holds x "/\" lim N in Lim (x "/\" N); theorem :: WAYBEL_9:27 for S being Hausdorff TopLattice, x being Element of S st for a being Element of S holds a"/\" is continuous holds uparrow x is closed; theorem :: WAYBEL_9:28 for S being compact Hausdorff TopLattice, x being Element of S st for b being Element of S holds b"/\" is continuous holds downarrow x is closed; begin :: The Cluster Points of Nets definition let T be non empty TopSpace, N be non empty NetStr over T, p be Point of T; pred p is_a_cluster_point_of N means :: WAYBEL_9:def 9 for O being a_neighborhood of p holds N is_often_in O; end; theorem :: WAYBEL_9:29 for L being non empty TopSpace, N being net of L for c being Point of L st c in Lim N holds c is_a_cluster_point_of N; theorem :: WAYBEL_9:30 for T being compact Hausdorff non empty TopSpace, N being net of T ex c being Point of T st c is_a_cluster_point_of N; theorem :: WAYBEL_9:31 for L being non empty TopSpace, N being net of L, M being subnet of N for c being Point of L st c is_a_cluster_point_of M holds c is_a_cluster_point_of N; theorem :: WAYBEL_9:32 for T being non empty TopSpace, N being net of T for x being Point of T st x is_a_cluster_point_of N holds ex M being subnet of N st x in Lim M; theorem :: WAYBEL_9:33 for L being compact Hausdorff non empty TopSpace, N being net of L st for c, d being Point of L st c is_a_cluster_point_of N & d is_a_cluster_point_of N holds c = d holds for s being Point of L st s is_a_cluster_point_of N holds s in Lim N; theorem :: WAYBEL_9:34 for S being non empty TopSpace, c being Point of S for N being net of S, A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds c in A; theorem :: WAYBEL_9:35 for S being compact Hausdorff TopLattice, c being Point of S for N being net of S st (for x being Element of S holds x"/\" is continuous) & N is eventually-directed & c is_a_cluster_point_of N holds c = sup N; theorem :: WAYBEL_9:36 for S being compact Hausdorff TopLattice, c being Point of S for N being net of S st (for x being Element of S holds x"/\" is continuous) & N is eventually-filtered & c is_a_cluster_point_of N holds c = inf N; begin :: On The Topological Properties of Meet-Continuous Lattices :: Proposition 4.4 s. 32 (i) & (ii) => MC theorem :: WAYBEL_9:37 for S being Hausdorff TopLattice st (for N being net of S st N is eventually-directed holds ex_sup_of N & sup N in Lim N) & (for x being Element of S holds x"/\" is continuous) holds S is meet-continuous; :: Proposition 4.4 s. 32 (ii) => (i) theorem :: WAYBEL_9:38 for S being compact Hausdorff TopLattice st for x being Element of S holds x"/\" is continuous holds for N being net of S st N is eventually-directed holds ex_sup_of N & sup N in Lim N; :: Proposition 4.4 s. 32 (ii) => (i) dual theorem :: WAYBEL_9:39 for S being compact Hausdorff TopLattice st for x being Element of S holds x"/\" is continuous holds for N being net of S st N is eventually-filtered holds ex_inf_of N & inf N in Lim N; theorem :: WAYBEL_9:40 for S being compact Hausdorff TopLattice st for x being Element of S holds x"/\" is continuous holds S is bounded; theorem :: WAYBEL_9:41 for S being compact Hausdorff TopLattice st for x being Element of S holds x"/\" is continuous holds S is meet-continuous;