:: The Lawson Topology :: by Grzegorz Bancerek :: :: Received June 21, 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 XBOOLE_0, WAYBEL_9, WAYBEL_0, SUBSET_1, CANTOR_1, ORDERS_2, ZFMISC_1, RELAT_2, PRE_TOPC, STRUCT_0, RLVECT_3, TARSKI, SETFAM_1, XXREAL_0, REWRITE1, PRELAMB, YELLOW_9, ORDINAL1, RCOMP_1, FINSET_1, FUNCT_1, RELAT_1, ORDINAL2, YELLOW_0, LATTICES, CAT_1, ARYTM_0, LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, CONNSP_2, TOPS_1, PROB_1, WAYBEL11, DIRAF, CARD_FIL, YELLOW_1, EQREL_1, COMPTS_1, WAYBEL19, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FINSET_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3, ORDERS_3, PRE_TOPC, TOPS_1, CONNSP_2, BORSUK_1, COMPTS_1, YELLOW_0, WAYBEL_0, YELLOW_1, CANTOR_1, YELLOW_3, WAYBEL_2, YELLOW_6, YELLOW_7, WAYBEL_3, WAYBEL_9, WAYBEL11, YELLOW_9; constructors TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3, CANTOR_1, ORDERS_3, WAYBEL_3, WAYBEL11, YELLOW_9, COMPTS_1, WAYBEL_2; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, BORSUK_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3, YELLOW_6, WAYBEL11, YELLOW_9, YELLOW12, TOPS_1; requirements BOOLE, SUBSET; begin :: Lower topoplogy definition :: 1.1. DEFINITION, p. 142 (part I) let T be non empty TopRelStr; attr T is lower means :: WAYBEL19:def 1 the set of all (uparrow x)` where x is Element of T is prebasis of T; end; registration cluster -> lower for 1-element reflexive TopSpace-like TopRelStr; end; registration cluster lower trivial complete strict for TopLattice; end; theorem :: WAYBEL19:1 for LL being non empty RelStr ex T being strict correct TopAugmentation of LL st T is lower; registration let R be non empty RelStr; cluster lower for strict correct TopAugmentation of R; end; theorem :: WAYBEL19:2 for L1,L2 being TopSpace-like lower non empty TopRelStr st the RelStr of L1 = the RelStr of L2 holds the topology of L1 = the topology of L2 ; definition :: 1.1. DEFINITION, p. 142 (part II) let R be non empty RelStr; func omega R -> Subset-Family of R means :: WAYBEL19:def 2 for T being lower correct TopAugmentation of R holds it = the topology of T; end; theorem :: WAYBEL19:3 for R1,R2 being non empty RelStr st the RelStr of R1 = the RelStr of R2 holds omega R1 = omega R2; theorem :: WAYBEL19:4 for T being lower non empty TopRelStr for x being Point of T holds (uparrow x)` is open & uparrow x is closed; theorem :: WAYBEL19:5 for T being transitive lower non empty TopRelStr for A being Subset of T st A is open holds A is lower; theorem :: WAYBEL19:6 for T being transitive lower non empty TopRelStr for A being Subset of T st A is closed holds A is upper; theorem :: WAYBEL19:7 for T being non empty TopSpace-like TopRelStr holds T is lower iff {(uparrow F)` where F is Subset of T: F is finite} is Basis of T; theorem :: WAYBEL19:8 :: 1.2. LEMMA, (i) generalized, p. 143 for S,T being lower complete TopLattice, f being Function of S, T st for X being non empty Subset of S holds f preserves_inf_of X holds f is continuous; theorem :: WAYBEL19:9 :: 1.2. LEMMA (i), p. 143 for S,T being lower complete TopLattice, f being Function of S, T st f is infs-preserving holds f is continuous; theorem :: WAYBEL19:10 for T being lower complete TopLattice, BB being prebasis of T for F being non empty filtered Subset of T st for A being Subset of T st A in BB & inf F in A holds F meets A holds inf F in Cl F; theorem :: WAYBEL19:11 :: 1.2. LEMMA (ii), p. 143 for S,T being lower complete TopLattice for f being Function of S,T st f is continuous holds f is filtered-infs-preserving; theorem :: WAYBEL19:12 :: 1.2. LEMMA (iii), p. 143 for S,T being lower complete TopLattice for f being Function of S,T st f is continuous & for X being finite Subset of S holds f preserves_inf_of X holds f is infs-preserving; theorem :: WAYBEL19:13 :: Remark before 1.3., p. 143 for T being lower TopSpace-like reflexive transitive non empty TopRelStr for x being Point of T holds Cl {x} = uparrow x; definition mode TopPoset is TopSpace-like reflexive transitive antisymmetric TopRelStr; end; registration :: Remark before 1.3., p. 143 cluster lower -> T_0 for non empty TopPoset; end; registration let R be lower-bounded non empty RelStr; cluster -> lower-bounded for TopAugmentation of R; end; theorem :: WAYBEL19:14 for S, T being non empty RelStr, s being Element of S, t being Element of T holds (uparrow [s,t])` = [:(uparrow s)`, the carrier of T:] \/ [: the carrier of S, (uparrow t)`:]; theorem :: WAYBEL19:15 :: 1.3. LEMMA, p. 143 (variant I) for S,T being lower-bounded non empty Poset for S9 being lower correct TopAugmentation of S for T9 being lower correct TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9 qua non empty TopSpace:]; theorem :: WAYBEL19:16 :: 1.3. LEMMA, p. 143 (variant II) for S,T being lower lower-bounded non empty TopPoset holds omega [:S ,T qua Poset:] = the topology of [:S,T qua non empty TopSpace:]; theorem :: WAYBEL19:17 :: 1.4. LEMMA, p. 144:: Refinements for T,T2 being lower complete TopLattice st T2 is TopAugmentation of [:T, T qua LATTICE:] for f being Function of T2,T st f = inf_op T holds f is continuous; begin :: Refinements scheme :: WAYBEL19:sch 1 TopInd {T() -> TopLattice, P[set]}: for A being Subset of T() st A is open holds P[A] provided ex K being prebasis of T() st for A being Subset of T() st A in K holds P[A] and for F being Subset-Family of T() st for A being Subset of T() st A in F holds P[A] holds P[union F] and for A1,A2 being Subset of T() st P[A1] & P[A2] holds P[A1 /\ A2] and P[[#]T()]; theorem :: WAYBEL19:18 for L1,L2 being up-complete antisymmetric non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 & for x being Element of L1 holds waybelow x is directed non empty holds L1 is satisfying_axiom_of_approximation implies L2 is satisfying_axiom_of_approximation; registration let T be continuous non empty Poset; cluster -> continuous for TopAugmentation of T; end; theorem :: WAYBEL19:19 for T,S being TopSpace, R being Refinement of T,S for W being Subset of R st W in the topology of T or W in the topology of S holds W is open ; theorem :: WAYBEL19:20 for T,S being TopSpace, R being Refinement of T,S for V being Subset of T, W being Subset of R st W = V holds V is open implies W is open; theorem :: WAYBEL19:21 for T,S being TopSpace st the carrier of T = the carrier of S for R being Refinement of T,S for V being Subset of T, W being Subset of R st W = V holds V is closed implies W is closed; theorem :: WAYBEL19:22 for T being non empty TopSpace, K,O being set st K c= O & O c= the topology of T holds (K is Basis of T implies O is Basis of T) & (K is prebasis of T implies O is prebasis of T); theorem :: WAYBEL19:23 :: YELLOW_9:58 revised for T1,T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 for T be Refinement of T1, T2 for B1 being prebasis of T1, B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T; theorem :: WAYBEL19:24 for T1,S1,T2,S2 being non empty TopSpace for R1 being Refinement of T1 ,S1, R2 being Refinement of T2,S2 for f being Function of T1,T2, g being Function of S1,S2 for h being Function of R1,R2 st h = f & h = g holds f is continuous & g is continuous implies h is continuous; theorem :: WAYBEL19:25 for T being non empty TopSpace, K being prebasis of T for N being net of T, p being Point of T st for A being Subset of T st p in A & A in K holds N is_eventually_in A holds p in Lim N; theorem :: WAYBEL19:26 for T being non empty TopSpace for N being net of T for S being Subset of T st N is_eventually_in S holds Lim N c= Cl S; theorem :: WAYBEL19:27 for R being non empty RelStr, X being non empty Subset of R holds the mapping of X+id = id X & the mapping of X opp+id = id X; theorem :: WAYBEL19:28 for R being reflexive antisymmetric non empty RelStr, x being Element of R holds (uparrow x) /\ (downarrow x) = {x}; begin :: Lawson topology definition let T be reflexive non empty TopRelStr; attr T is Lawson means :: WAYBEL19:def 3 (omega T) \/ (sigma T) is prebasis of T; end; theorem :: WAYBEL19:29 for R being complete LATTICE for LL being lower correct TopAugmentation of R for S being Scott TopAugmentation of R for T being correct TopAugmentation of R holds T is Lawson iff T is Refinement of S,LL; registration let R be complete LATTICE; cluster Lawson strict correct for TopAugmentation of R; end; registration cluster Scott complete strict for TopLattice; cluster Lawson continuous for complete strict TopLattice; end; theorem :: WAYBEL19:30 for T being Lawson complete TopLattice holds (sigma T) \/ the set of all ( uparrow x)` where x is Element of T is prebasis of T; theorem :: WAYBEL19:31 for T being Lawson complete TopLattice holds (sigma T) \/ {W\uparrow x where W is Subset of T, x is Element of T: W in sigma T} is prebasis of T; theorem :: WAYBEL19:32 for T being Lawson complete TopLattice holds {W\uparrow F where W,F is Subset of T: W in sigma T & F is finite} is Basis of T; definition :: 1.5. DEFINITION, p. 144 (part II) let T be complete LATTICE; func lambda T -> Subset-Family of T means :: WAYBEL19:def 4 for S being Lawson correct TopAugmentation of T holds it = the topology of S; end; theorem :: WAYBEL19:33 for R being complete LATTICE holds lambda R = UniCl FinMeetCl (( sigma R) \/ (omega R)); theorem :: WAYBEL19:34 for R being complete LATTICE for T being lower correct TopAugmentation of R for S being Scott correct TopAugmentation of R for M being Refinement of S ,T holds lambda R = the topology of M; theorem :: WAYBEL19:35 for T being lower up-complete TopLattice for A being Subset of T st A is open holds A is property(S); theorem :: WAYBEL19:36 :: Remark after 1.5. p. 144 for T being Lawson complete TopLattice for A being Subset of T st A is open holds A is property(S); theorem :: WAYBEL19:37 for S being Scott complete TopLattice for T being Lawson correct TopAugmentation of S for A being Subset of S st A is open for C being Subset of T st C = A holds C is open; theorem :: WAYBEL19:38 for T being Lawson complete TopLattice for x being Element of T holds uparrow x is closed & downarrow x is closed & {x} is closed; theorem :: WAYBEL19:39 for T being Lawson complete TopLattice for x being Element of T holds (uparrow x)` is open & (downarrow x)` is open & {x}` is open; theorem :: WAYBEL19:40 for T being Lawson complete continuous TopLattice for x being Element of T holds wayabove x is open & (wayabove x)` is closed; theorem :: WAYBEL19:41 :: 1.6. PROPOSITION (i), p. 144 for S being Scott complete TopLattice for T being Lawson correct TopAugmentation of S for A being upper Subset of T st A is open for C being Subset of S st C = A holds C is open; theorem :: WAYBEL19:42 :: 1.6. PROPOSITION (ii), p. 144 for T being Lawson complete TopLattice for A being lower Subset of T holds A is closed iff A is closed_under_directed_sups; theorem :: WAYBEL19:43 :: 1.7. LEMMA, p. 145 for T being Lawson complete TopLattice for F being non empty filtered Subset of T holds Lim (F opp+id) = {inf F}; registration :: 1.9. THEOREM, p. 146 cluster Lawson -> T_1 compact for complete TopLattice; end; registration :: 1.10. THEOREM, p. 146 cluster Lawson -> Hausdorff for complete continuous TopLattice; end;