:: Lawson Topology in Continuous Lattices :: by Grzegorz Bancerek :: :: Received July 12, 1998 :: Copyright (c) 1998-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 WAYBEL_0, LATTICES, FUNCT_1, FINSET_1, SUBSET_1, STRUCT_0, FUNCOP_1, YELLOW_0, XBOOLE_0, RELAT_1, ORDINAL2, TARSKI, SEQM_3, XXREAL_0, LATTICE3, ORDERS_2, REWRITE1, CAT_1, FUNCT_3, EQREL_1, WELLORD1, WAYBEL_5, PRE_TOPC, ORDINAL1, CONNSP_2, TOPS_1, RCOMP_1, RELAT_2, WAYBEL_9, ARYTM_0, WAYBEL19, YELLOW_6, WAYBEL11, CANTOR_1, YELLOW_9, PROB_1, YELLOW_2, PRELAMB, WAYBEL21; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, TOLER_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, COMPTS_1, CANTOR_1, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3, WAYBEL_5, YELLOW_6, YELLOW_7, WAYBEL_9, YELLOW_9, WAYBEL11, WAYBEL17, WAYBEL19; constructors TOLER_1, TOPS_1, NATTRA_1, BORSUK_1, CANTOR_1, TOPS_2, ORDERS_3, YELLOW_2, WAYBEL_3, WAYBEL17, YELLOW_9, WAYBEL19, COMPTS_1, WAYBEL_2; registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_2, YELLOW_6, WAYBEL_9, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL19, TOPS_1, RELSET_1; requirements SUBSET, BOOLE; begin :: Semilattice homomorphism and inheritance definition let S,T be Semilattice such that S is upper-bounded implies T is upper-bounded; mode SemilatticeHomomorphism of S,T -> Function of S,T means :: WAYBEL21:def 1 for X being finite Subset of S holds it preserves_inf_of X; end; registration let S,T be Semilattice; cluster meet-preserving -> monotone for Function of S,T; end; registration let S be Semilattice, T be upper-bounded Semilattice; cluster -> meet-preserving for SemilatticeHomomorphism of S,T; end; theorem :: WAYBEL21:1 for S,T being upper-bounded Semilattice for f being SemilatticeHomomorphism of S,T holds f.Top S = Top T; theorem :: WAYBEL21:2 for S,T being Semilattice, f being Function of S,T st f is meet-preserving for X being finite non empty Subset of S holds f preserves_inf_of X; theorem :: WAYBEL21:3 for S,T being upper-bounded Semilattice, f being meet-preserving Function of S, T st f.Top S = Top T holds f is SemilatticeHomomorphism of S,T; theorem :: WAYBEL21:4 for S,T being Semilattice, f being Function of S,T st f is meet-preserving & for X being filtered non empty Subset of S holds f preserves_inf_of X for X being non empty Subset of S holds f preserves_inf_of X; theorem :: WAYBEL21:5 for S,T being Semilattice, f being Function of S,T st f is infs-preserving holds f is SemilatticeHomomorphism of S,T; theorem :: WAYBEL21:6 for S1,T1,S2,T2 being non empty RelStr st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2 for f1 being Function of S1,T1, f2 being Function of S2,T2 st f1 = f2 holds (f1 is infs-preserving implies f2 is infs-preserving) & (f1 is directed-sups-preserving implies f2 is directed-sups-preserving); theorem :: WAYBEL21:7 for S1,T1,S2,T2 being non empty RelStr st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2 for f1 being Function of S1,T1, f2 being Function of S2,T2 st f1 = f2 holds (f1 is sups-preserving implies f2 is sups-preserving) & (f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving); theorem :: WAYBEL21:8 for T being complete LATTICE for S being infs-inheriting full non empty SubRelStr of T holds incl(S,T) is infs-preserving; theorem :: WAYBEL21:9 for T being complete LATTICE for S being sups-inheriting full non empty SubRelStr of T holds incl(S,T) is sups-preserving; theorem :: WAYBEL21:10 for T being up-complete non empty Poset for S being directed-sups-inheriting full non empty SubRelStr of T holds incl(S,T) is directed-sups-preserving; theorem :: WAYBEL21:11 for T being complete LATTICE for S being filtered-infs-inheriting full non empty SubRelStr of T holds incl(S,T) is filtered-infs-preserving; theorem :: WAYBEL21:12 for T1,T2,R being RelStr, S being SubRelStr of T1 st the RelStr of T1 = the RelStr of T2 & the RelStr of S = the RelStr of R holds R is SubRelStr of T2 & (S is full implies R is full SubRelStr of T2); theorem :: WAYBEL21:13 for T being non empty RelStr holds T is infs-inheriting sups-inheriting full SubRelStr of T; registration let T be complete LATTICE; cluster complete for CLSubFrame of T; end; theorem :: WAYBEL21:14 for T being Semilattice for S being full non empty SubRelStr of T holds S is meet-inheriting iff for X being finite non empty Subset of S holds "/\" (X, T) in the carrier of S; theorem :: WAYBEL21:15 for T being sup-Semilattice for S being full non empty SubRelStr of T holds S is join-inheriting iff for X being finite non empty Subset of S holds "\/" (X, T) in the carrier of S; theorem :: WAYBEL21:16 for T being upper-bounded Semilattice for S being meet-inheriting full non empty SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds S is infs-inheriting; theorem :: WAYBEL21:17 for T being lower-bounded sup-Semilattice for S being join-inheriting full non empty SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds S is sups-inheriting; theorem :: WAYBEL21:18 for T being complete LATTICE, S being full non empty SubRelStr of T st S is infs-inheriting holds S is complete; theorem :: WAYBEL21:19 for T being complete LATTICE, S being full non empty SubRelStr of T st S is sups-inheriting holds S is complete; theorem :: WAYBEL21:20 for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is infs-inheriting implies S2 is infs-inheriting; theorem :: WAYBEL21:21 for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is sups-inheriting implies S2 is sups-inheriting; theorem :: WAYBEL21:22 for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting; theorem :: WAYBEL21:23 for T1,T2 being non empty RelStr for S1 being non empty full SubRelStr of T1 for S2 being non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting; begin :: Nets and limits theorem :: WAYBEL21:24 for S,T being non empty TopSpace, N being net of S for f being Function of S,T st f is continuous holds f.:Lim N c= Lim (f*N); definition let T be non empty RelStr; let N be non empty NetStr over T; redefine attr N is antitone means :: WAYBEL21:def 2 for i,j being Element of N st i <= j holds N.i >= N.j; end; registration let T be non empty reflexive RelStr; let x be Element of T; cluster {x} opp+id -> transitive directed monotone antitone; end; registration let T be non empty reflexive RelStr; cluster monotone antitone reflexive strict for net of T; end; registration let T be non empty RelStr; let F be non empty Subset of T; cluster F opp+id -> antitone; end; registration let S,T be non empty reflexive RelStr; let f be monotone Function of S,T; let N be antitone non empty NetStr over S; cluster f*N -> antitone; end; theorem :: WAYBEL21:25 for S being complete LATTICE, N be net of S holds the set of all "/\"({N.i where i is Element of N:i >= j},S) where j is Element of N is directed non empty Subset of S; theorem :: WAYBEL21:26 for S being non empty Poset, N be monotone reflexive net of S holds the set of all "/\"({N.i where i is Element of N: i >= j}, S) where j is Element of N is directed non empty Subset of S; theorem :: WAYBEL21:27 for S being non empty 1-sorted, N being non empty NetStr over S, X being set st rng the mapping of N c= X holds N is_eventually_in X; theorem :: WAYBEL21:28 for R being /\-complete non empty Poset for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F; theorem :: WAYBEL21:29 for S,T being /\-complete non empty Poset for X being non empty filtered Subset of S for f being monotone Function of S,T holds lim_inf (f*(X opp+id)) = inf (f.:X); theorem :: WAYBEL21:30 for S,T being non empty TopPoset for X being non empty filtered Subset of S for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f.:X holds f*(X opp+id) is subnet of Y opp+id; theorem :: WAYBEL21:31 for S,T being non empty TopPoset for X being non empty filtered Subset of S for f being monotone Function of S,T for Y being non empty filtered Subset of T st Y = f.:X holds Lim (Y opp+id) c= Lim (f*(X opp+id)); theorem :: WAYBEL21:32 for S being non empty reflexive RelStr, D being non empty Subset of S holds the mapping of Net-Str D = id D & the carrier of Net-Str D = D & Net-Str D is full SubRelStr of S; theorem :: WAYBEL21:33 for S,T being up-complete non empty Poset for f being monotone Function of S,T for D being non empty directed Subset of S holds lim_inf (f*Net-Str D) = sup (f.:D); theorem :: WAYBEL21:34 for S being non empty reflexive RelStr for D being non empty directed Subset of S for i,j being Element of Net-Str D holds i <= j iff (Net-Str D).i <= (Net-Str D).j; theorem :: WAYBEL21:35 for T being Lawson complete TopLattice for D being directed non empty Subset of T holds sup D in Lim Net-Str D; definition let T be non empty 1-sorted; let N be net of T, M be non empty NetStr over T such that M is subnet of N; mode Embedding of M,N -> Function of M,N means :: WAYBEL21:def 3 the mapping of M = (the mapping of N)*it & for m being Element of N ex n being Element of M st for p being Element of M st n <= p holds m <= it.p; end; theorem :: WAYBEL21:36 for T being non empty 1-sorted for N being net of T, M being subnet of N for e being Embedding of M,N, i being Element of M holds M.i = N.(e.i); theorem :: WAYBEL21:37 for T being complete LATTICE for N being net of T, M being subnet of N holds lim_inf N <= lim_inf M; theorem :: WAYBEL21:38 for T being complete LATTICE for N being net of T, M being subnet of N for e being Embedding of M, N st for i being Element of N, j being Element of M st e.j <= i ex j9 being Element of M st j9 >= j & N.i >= M.j9 holds lim_inf N = lim_inf M; theorem :: WAYBEL21:39 for T being non empty RelStr for N being net of T, M being non empty full SubNetStr of N st for i being Element of N ex j being Element of N st j >= i & j in the carrier of M holds M is subnet of N & incl(M,N) is Embedding of M,N; theorem :: WAYBEL21:40 for T being non empty RelStr, N being net of T for i being Element of N holds N|i is subnet of N & incl(N|i,N) is Embedding of N|i, N; theorem :: WAYBEL21:41 for T being complete LATTICE, N being net of T for i being Element of N holds lim_inf (N|i) = lim_inf N; theorem :: WAYBEL21:42 for T being non empty RelStr, N being net of T, X being set st N is_eventually_in X ex i be Element of N st N.i in X & rng the mapping of N|i c= X; theorem :: WAYBEL21:43 :: see WAYBEL_2:18, for eventually-directed for T being Lawson complete TopLattice for N being eventually-filtered net of T holds rng the mapping of N is filtered non empty Subset of T; theorem :: WAYBEL21:44 :: 1.7. LEMMA, -- WAYBEL19:44 revised for T being Lawson complete TopLattice for N being eventually-filtered net of T holds Lim N = {inf N}; begin :: Lawson topology revisited theorem :: WAYBEL21:45 :: 1.8. THEOREM, (1) <=> (2), generalized, p. 145 for S,T being Lawson complete TopLattice for f being meet-preserving Function of S,T holds f is continuous iff f is directed-sups-preserving & for X being non empty Subset of S holds f preserves_inf_of X; theorem :: WAYBEL21:46 :: 1.8. THEOREM, (1) <=> (2), p. 145 for S,T being Lawson complete TopLattice for f being SemilatticeHomomorphism of S,T holds f is continuous iff f is infs-preserving directed-sups-preserving; definition let S,T be non empty RelStr; let f be Function of S,T; attr f is lim_infs-preserving means :: WAYBEL21:def 4 for N being net of S holds f.lim_inf N = lim_inf (f*N); end; theorem :: WAYBEL21:47 :: 1.8. THEOREM, (1) <=> (3), p. 145 for S,T being Lawson complete TopLattice for f being SemilatticeHomomorphism of S,T holds f is continuous iff f is lim_infs-preserving; theorem :: WAYBEL21:48 :: 1.11. THEOREM, (1) => (2a), p. 147 for T being Lawson complete continuous TopLattice for S being meet-inheriting full non empty SubRelStr of T st Top T in the carrier of S & ex X being Subset of T st X = the carrier of S & X is closed holds S is infs-inheriting; theorem :: WAYBEL21:49 :: 1.11. THEOREM, (1) => (2b), p. 147 for T being Lawson complete continuous TopLattice for S being full non empty SubRelStr of T st ex X being Subset of T st X = the carrier of S & X is closed holds S is directed-sups-inheriting; theorem :: WAYBEL21:50 :: 1.11. THEOREM, (2) => (1), p. 147 for T being Lawson complete continuous TopLattice for S being infs-inheriting directed-sups-inheriting full non empty SubRelStr of T ex X being Subset of T st X = the carrier of S & X is closed; theorem :: WAYBEL21:51 :: 1.11. THEOREM, (2) => (3+), p. 147 for T being Lawson complete continuous TopLattice for S being infs-inheriting directed-sups-inheriting full non empty SubRelStr of T for N being net of T st N is_eventually_in the carrier of S holds lim_inf N in the carrier of S; theorem :: WAYBEL21:52 :: 1.11. THEOREM, (3) => (2a), p. 147 for T being Lawson complete continuous TopLattice for S being meet-inheriting full non empty SubRelStr of T st Top T in the carrier of S & for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S holds S is infs-inheriting; theorem :: WAYBEL21:53 :: 1.11. THEOREM, (3) => (2b), p. 147 for T being Lawson complete continuous TopLattice for S being full non empty SubRelStr of T st for N being net of T st rng the mapping of N c= the carrier of S holds lim_inf N in the carrier of S holds S is directed-sups-inheriting; theorem :: WAYBEL21:54 :: 1.11. THEOREM, (1) <=> (3+), p. 147 for T being Lawson complete continuous TopLattice for S being meet-inheriting full non empty SubRelStr of T for X being Subset of T st X = the carrier of S & Top T in X holds X is closed iff for N being net of T st N is_eventually_in X holds lim_inf N in X;