Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### The Lawson Topology

**by****Grzegorz Bancerek**- Received June 21, 1998
- MML identifier: WAYBEL19

- [ Mizar article, MML identifier index ]

environ vocabulary WAYBEL_9, WAYBEL_0, CANTOR_1, ORDERS_1, SUBSET_1, BOOLE, REALSET1, RELAT_2, PRE_TOPC, SETFAM_1, BHSP_3, PRELAMB, YELLOW_9, TARSKI, ORDINAL2, FINSET_1, FUNCT_1, RELAT_1, YELLOW_0, LATTICES, CAT_1, OPPCAT_1, SEQM_3, LATTICE3, TSP_1, WAYBEL_2, WAYBEL_3, QUANTAL1, CONNSP_2, TOPS_1, PROB_1, WAYBEL11, DIRAF, URYSOHN1, COMPTS_1, YELLOW_1, YELLOW_6, WAYBEL19, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0, REALSET1, FUNCT_2, ORDERS_1, LATTICE3, ORDERS_3, PRE_TOPC, TOPS_1, TOPS_2, TSP_1, BORSUK_1, URYSOHN1, 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 ORDERS_3, WAYBEL_1, CANTOR_1, TOPS_1, TOPS_2, WAYBEL_3, TSP_1, WAYBEL11, TDLAT_3, URYSOHN1, YELLOW_9, LATTICE3, MEMBERED; clusters STRUCT_0, LATTICE3, WAYBEL_0, FINSET_1, BORSUK_1, YELLOW_1, YELLOW_3, YELLOW_6, WAYBEL_3, WAYBEL_9, WAYBEL11, YELLOW_9, YELLOW12, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_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 {(uparrow x)` where x is Element of T: not contradiction} is prebasis of T; end; definition cluster trivial -> lower (non empty reflexive TopSpace-like TopRelStr); end; definition cluster lower trivial complete strict TopLattice; end; theorem :: WAYBEL19:1 for LL being non empty RelStr ex T being strict correct TopAugmentation of LL st T is lower; definition let R be non empty RelStr; cluster lower (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 map 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 map 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 map 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 map 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; definition :: Remark before 1.3., p. 143 cluster lower -> T_0 (non empty TopPoset); end; definition let R be lower-bounded non empty RelStr; cluster -> lower-bounded 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 S' being lower correct TopAugmentation of S for T' being lower correct TopAugmentation of T holds omega [:S,T:] = the topology of [:S',T' 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 for T,T2 being lower complete TopLattice st T2 is TopAugmentation of [:T, T qua LATTICE:] for f being map of T2,T st f = inf_op T holds f is continuous; begin :: Refinements scheme 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; definition let T be continuous (non empty Poset); cluster -> continuous 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 map of T1,T2, g being map of S1,S2 for h being map 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 :: 1.5. DEFINITION, p. 144 (part I) 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; definition let R be complete LATTICE; cluster Lawson strict correct TopAugmentation of R; end; definition cluster Scott complete strict TopLattice; cluster Lawson continuous (complete strict TopLattice); end; theorem :: WAYBEL19:30 for T being Lawson (complete TopLattice) holds (sigma T) \/ {(uparrow x)` where x is Element of T: not contradiction} 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 has_the_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 has_the_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}; definition :: 1.9. THEOREM, p. 146 cluster Lawson -> being_T1 compact (complete TopLattice); end; definition :: 1.10. THEOREM, p. 146 cluster Lawson -> Hausdorff (complete continuous TopLattice); end;

Back to top