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;