The abstract of the Mizar article:

The Scott Topology. Part II

by

Czeslaw Bylinski, and

Piotr Rudnicki

Received August 27, 1997

MML identifier: WAYBEL14

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSET_1, SETFAM_1, TARSKI, BOOLE, CARD_1, SUBSET_1, RELAT_2,
      LATTICE3, ORDERS_1, WAYBEL_0, LATTICES, BHSP_3, ORDINAL2, WAYBEL_3,
      WAYBEL_6, RELAT_1, FILTER_0, WAYBEL_8, QUANTAL1, COMPTS_1, PRE_TOPC,
      YELLOW_1, WAYBEL_9, CANTOR_1, WAYBEL11, PROB_1, YELLOW_6, WAYBEL_2,
      FUNCT_1, TMAP_1, CONNSP_2, TOPS_1, YELLOW_8, TSP_1, YELLOW_0, WAYBEL_5,
      OPPCAT_1, WAYBEL14, RLVECT_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, SETFAM_1, FINSET_1,
      DOMAIN_1, FUNCT_1, ORDERS_1, LATTICE3, CARD_1, STRUCT_0, PRE_TOPC,
      TOPS_1, TOPS_2, CONNSP_2, BORSUK_1, TMAP_1, CANTOR_1, TSP_1, COMPTS_1,
      YELLOW_0, YELLOW_1, YELLOW_3, YELLOW_4, YELLOW_6, YELLOW_7, YELLOW_8,
      WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8,
      WAYBEL_9, WAYBEL11;
 constructors NAT_1, DOMAIN_1, TOPS_1, TOPS_2, TMAP_1, CANTOR_1, T_0TOPSP,
      YELLOW_4, YELLOW_8, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8,
      WAYBEL11, BORSUK_1, MEMBERED;
 clusters SUBSET_1, STRUCT_0, FINSET_1, LATTICE3, BORSUK_1, PRE_TOPC, CANTOR_1,
      YELLOW_1, YELLOW_4, YELLOW_6, YELLOW_8, WAYBEL_0, WAYBEL_3, WAYBEL_6,
      WAYBEL_7, WAYBEL_8, WAYBEL11, RELSET_1, MEMBERED, ZFMISC_1;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

theorem :: WAYBEL14:1
for X being set, F being finite Subset-Family of X
 ex G being finite Subset-Family of X st G c= F & union G = union F &
  for g being Subset of X st g in G holds not g c= union (G\{g});

theorem :: WAYBEL14:2
 for S being 1-sorted, X being Subset of S
  holds X` = the carrier of S iff X is empty;

theorem :: WAYBEL14:3
for R being antisymmetric with_infima transitive non empty RelStr,
    x, y being Element of R
 holds downarrow (x"/\"y) = (downarrow x) /\ downarrow y;

theorem :: WAYBEL14:4
  for R being antisymmetric with_suprema transitive non empty RelStr,
    x, y being Element of R
 holds uparrow (x"\/"y) = (uparrow x) /\ uparrow y;

theorem :: WAYBEL14:5
for L being complete antisymmetric (non empty RelStr),
    X being lower Subset of L
 st sup X in X holds X = downarrow sup X;

theorem :: WAYBEL14:6
  for L being complete antisymmetric (non empty RelStr),
    X being upper Subset of L
 st inf X in X holds X = uparrow inf X;

theorem :: WAYBEL14:7
 for R being non empty reflexive transitive RelStr, x, y being Element of R
  holds x << y iff uparrow y c= wayabove x;

theorem :: WAYBEL14:8
   for R being non empty reflexive transitive RelStr, x, y being Element of R
  holds x << y iff downarrow x c= waybelow y;

theorem :: WAYBEL14:9
for R being complete reflexive antisymmetric (non empty RelStr),
    x being Element of R
 holds sup waybelow x <= x & x <= inf wayabove x;

theorem :: WAYBEL14:10
for L being lower-bounded antisymmetric non empty RelStr
 holds uparrow Bottom L = the carrier of L;

theorem :: WAYBEL14:11
  for L being upper-bounded antisymmetric non empty RelStr
 holds downarrow Top L = the carrier of L;

theorem :: WAYBEL14:12
for P being with_suprema Poset, x, y being Element of P
 holds (wayabove x)"\/"(wayabove y) c= uparrow (x"\/"y);

theorem :: WAYBEL14:13
  for P being with_infima Poset, x, y being Element of P
 holds (waybelow x)"/\"(waybelow y) c= downarrow (x"/\"y);

theorem :: WAYBEL14:14
for R being with_suprema non empty Poset, l being Element of R holds
 l is co-prime iff
 for x,y be Element of R st l <= x "\/" y holds l <= x or l <= y;

theorem :: WAYBEL14:15
for P being complete (non empty Poset),
    V being non empty Subset of P
 holds downarrow inf V = meet {downarrow u where u is Element of P : u in V};

theorem :: WAYBEL14:16
  for P being complete (non empty Poset),
    V being non empty Subset of P
 holds uparrow sup V = meet {uparrow u where u is Element of P : u in V};

definition let L be sup-Semilattice,
               x be Element of L;
 cluster compactbelow x -> directed;
end;

theorem :: WAYBEL14:17
        :: See a parenthetical remark in the middle of p. 106.
        :: This fact is needed in the proof of II-1.11(ii), p. 105.
 for T being non empty TopSpace, S being irreducible Subset of T,
     V being Element of InclPoset the topology of T
   st V = S` holds V is prime;

theorem :: WAYBEL14:18
for T being non empty TopSpace,
    x, y be Element of InclPoset the topology of T
 holds x "\/" y = x \/ y & x "/\" y = x /\ y;

theorem :: WAYBEL14:19
for T being non empty TopSpace,
    V being Element of InclPoset the topology of T
 holds V is prime iff
       for X, Y being Element of InclPoset the topology of T
        st X/\Y c= V holds X c= V or Y c= V;

theorem :: WAYBEL14:20
  for T being non empty TopSpace,
    V being Element of InclPoset the topology of T
 holds V is co-prime iff
       for X, Y being Element of InclPoset the topology of T
        st V c= X \/ Y holds V c= X or V c= Y;

definition let T be non empty TopSpace;
 cluster InclPoset the topology of T -> distributive;
end;

theorem :: WAYBEL14:21
for T being non empty TopSpace, L being TopLattice,
    t being Point of T, l being Point of L,
    X being Subset-Family of L
 st the TopStruct of T = the TopStruct of L & t = l & X is Basis of l
  holds X is Basis of t;

theorem :: WAYBEL14:22
for L being TopLattice, x being Element of L
 st for X being Subset of L st X is open holds X is upper
  holds uparrow x is compact;

begin :: Scott topology, continuation of WAYBEl11

 reserve L for complete Scott TopLattice,
         x for Element of L,
         X, Y for Subset of L,
         V, W for Element of InclPoset sigma L,
         VV for Subset of InclPoset sigma L;

definition let L be complete LATTICE;
 cluster sigma L -> non empty;
end;

theorem :: WAYBEL14:23
 sigma L = the topology of L;

theorem :: WAYBEL14:24
 X in sigma L iff X is open;

theorem :: WAYBEL14:25
for X being filtered Subset of L
 st VV = {(downarrow x)` : x in X} holds VV is directed;

theorem :: WAYBEL14:26
 X is open & x in X implies inf X << x;

           :: p. 105
definition let R be non empty reflexive RelStr, f be map of [:R, R:], R;
 attr f is jointly_Scott-continuous means
:: WAYBEL14:def 1
 for T being non empty TopSpace
       st the TopStruct of T = ConvergenceSpace Scott-Convergence R
        ex ft being map of [:T, T:], T st ft = f & ft is continuous;
end;

theorem :: WAYBEL14:27  :: Proposition 1.11 (i) p. 105
 V = X implies (V is co-prime iff X is filtered upper);

theorem :: WAYBEL14:28 :: Proposition 1.11 (ii) p. 105
   (V = X & ex x st X = (downarrow x)`)
     implies V is prime & V <> the carrier of
L;

theorem :: WAYBEL14:29  :: Proposition 1.11 (iii) p. 105
 V = X & sup_op L is jointly_Scott-continuous & V is prime &
 V <> the carrier of L
  implies ex x st X = (downarrow x)`;

theorem :: WAYBEL14:30  :: Proposition 1.11 (iv) p. 105
 L is continuous implies sup_op L is jointly_Scott-continuous;

theorem :: WAYBEL14:31  :: Corollary 1.12 p. 106
 sup_op L is jointly_Scott-continuous implies L is sober;

theorem :: WAYBEL14:32 :: Corollary 1.13 p. 106
   L is continuous implies L is compact locally-compact sober Baire;

theorem :: WAYBEL14:33  :: Theorem 1.14 (1) implies (2) p. 107
L is continuous & X in sigma L implies X = union {wayabove x : x in X};

theorem :: WAYBEL14:34 :: Theorem 1.14 (2) implies (1) p. 107
   (for X st X in sigma L holds X = union {wayabove x : x in X})
   implies L is continuous;

theorem :: WAYBEL14:35 :: Theorem 1.14 (1) implies (3 first conjunct) p. 107
   L is continuous implies
  ex B being Basis of x st for X st X in B holds X is open filtered;

theorem :: WAYBEL14:36 :: Theorem 1.14 (1) implies (3 second conjunct) p. 107
  L is continuous implies InclPoset sigma L is continuous;

theorem :: WAYBEL14:37  :: Theorem 1.14 (3) implies (4) p. 107
 (for x ex B being Basis of x st for Y st Y in B holds Y is open filtered) &
 InclPoset sigma L is continuous
  implies x = "\/" ({inf X : x in X & X in sigma L}, L);

theorem :: WAYBEL14:38  :: Theorem 1.14 (4) implies (1) p. 107
 (for x holds x = "\/" ({inf X : x in X & X in sigma L}, L))
   implies L is continuous;

theorem :: WAYBEL14:39  :: Theorem 1.14 (3) iff (5) p. 107
  :: The conjunct InclPoset sigma L is continuous is dropped

    (for x ex B being Basis of x st for Y st Y in B holds Y is open filtered)
iff (for V ex VV st V = sup VV & for W st W in VV holds W is co-prime);

theorem :: WAYBEL14:40 :: Theorem 1.14 (5) iff (6) p. 107
      (for V ex VV st V = sup VV & for W st W in VV holds W is co-prime)
  & InclPoset sigma L is continuous
iff InclPoset sigma L is completely-distributive;

theorem :: WAYBEL14:41 :: Theorem 1.14 (6) iff (7) p. 107
      InclPoset sigma L is completely-distributive
iff InclPoset sigma L is continuous & (InclPoset sigma L) opp is continuous;

theorem :: WAYBEL14:42 :: Corollary 1.15 (1) implies (2) p. 108
  L is algebraic implies
 ex B being Basis of L st B = {uparrow x : x in
 the carrier of CompactSublatt L};

theorem :: WAYBEL14:43 :: Corollary 1.15 (2) implies (3) p. 108
  (ex B being Basis of L st B = {uparrow x :x in
 the carrier of CompactSublatt L})
  implies InclPoset sigma L is algebraic &
          for V ex VV st V = sup VV & for W st W in VV holds W is co-prime;

theorem :: WAYBEL14:44 :: Corollary 1.15 (3) implies (2) p. 108
        :: The proof of ((3) implies (1)) is split into two parts
        :: This one proves ((3) implies (2)) and the next is ((2) implies (1)).
   InclPoset sigma L is algebraic &
 (for V ex VV st V = sup VV & for W st W in VV holds W is co-prime)
implies
 ex B being Basis of L st B = {uparrow x : x in
 the carrier of CompactSublatt L};

theorem :: WAYBEL14:45 :: Corollary 1.15 (2) implies (1) p. 108
  (ex B being Basis of L st B = {uparrow x :x in
 the carrier of CompactSublatt L})
 implies L is algebraic;