The abstract of the Mizar article:

Injective Spaces. Part II

by

Artur Kornilowicz, and

Jaroslaw Gryko

Received July 3, 1999

MML identifier: WAYBEL25

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, WAYBEL18, BOOLE, SUBSET_1, URYSOHN1, BHSP_3, WAYBEL11,
      METRIC_1, WAYBEL_9, FUNCTOR0, T_0TOPSP, YELLOW_9, CARD_3, FUNCOP_1,
      YELLOW_1, RELAT_1, RLVECT_2, FUNCT_1, ORDERS_1, WAYBEL_0, CAT_1, TOPS_2,
      ORDINAL2, WELLORD1, GROUP_6, FUNCT_3, WAYBEL_1, BORSUK_1, LATTICES,
      QUANTAL1, LATTICE3, YELLOW_0, WAYBEL_3, RELAT_2, PROB_1, BINOP_1, SEQM_3,
      WAYBEL24, FUNCT_2, GROUP_1, PRALG_2, PRALG_1, YELLOW_2, REALSET1,
      CONNSP_2, TOPS_1, SEQ_2, COMPTS_1, YELLOW_8, TARSKI, SETFAM_1, WAYBEL25;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1,
      FUNCT_1, PARTFUN1, FUNCT_2, REALSET1, NATTRA_1, TOLER_1, QUANTAL1,
      CARD_3, PRALG_1, PRALG_2, PRE_CIRC, WAYBEL18, STRUCT_0, PRE_TOPC,
      GRCAT_1, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, TMAP_1, T_0TOPSP, URYSOHN1,
      BORSUK_3, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1,
      WAYBEL_2, YELLOW_6, WAYBEL_3, YELLOW_8, WAYBEL_9, WAYBEL11, YELLOW_9,
      WAYBEL17, YELLOW_1, WAYBEL24, YELLOW14;
 constructors BORSUK_3, CANTOR_1, ENUMSET1, GRCAT_1, NATTRA_1, ORDERS_3,
      PRALG_2, QUANTAL1, RELAT_2, TMAP_1, TOLER_1, TOPS_1, TOPS_2, URYSOHN1,
      WAYBEL_1, WAYBEL_8, WAYBEL17, WAYBEL24, YELLOW_8, YELLOW_9, YELLOW14,
      MONOID_0, MEMBERED;
 clusters BORSUK_3, FUNCT_1, LATTICE3, PRALG_1, PRE_TOPC, RELSET_1, STRUCT_0,
      TEX_1, TSP_1, TOPS_1, YELLOW_0, YELLOW_1, YELLOW_9, YELLOW12, WAYBEL_0,
      WAYBEL_2, WAYBEL_8, WAYBEL10, WAYBEL12, WAYBEL17, WAYBEL18, WAYBEL19,
      WAYBEL21, WAYBEL24, YELLOW14, SUBSET_1, BORSUK_1, MEMBERED, ZFMISC_1,
      FUNCT_2;
 requirements SUBSET, BOOLE;


begin  :: Injective spaces

theorem :: WAYBEL25:1
   for p being Point of Sierpinski_Space st p = 0 holds {p} is closed;

theorem :: WAYBEL25:2
 for p being Point of Sierpinski_Space st p = 1 holds {p} is non closed;

definition
 cluster Sierpinski_Space -> non being_T1;
end;

definition
 cluster complete Scott -> discerning TopLattice;
end;

definition
 cluster injective strict T_0-TopSpace;
end;

definition
 cluster complete Scott strict TopLattice;
end;

theorem :: WAYBEL25:3   :: see WAYBEL18:16
 for I being non empty set,
     T being Scott TopAugmentation of product(I --> BoolePoset 1) holds
   the carrier of T = the carrier of product(I --> Sierpinski_Space);

theorem :: WAYBEL25:4
 for L1, L2 being complete LATTICE,
     T1 being Scott TopAugmentation of L1,
     T2 being Scott TopAugmentation of L2,
     h being map of L1, L2, H being map of T1, T2 st h = H & h is isomorphic
  holds H is_homeomorphism;

theorem :: WAYBEL25:5
 for L1, L2 being complete LATTICE,
     T1 being Scott TopAugmentation of L1,
     T2 being Scott TopAugmentation of L2 st L1, L2 are_isomorphic holds
  T1, T2 are_homeomorphic;

theorem :: WAYBEL25:6
 for S, T being non empty TopSpace st S is injective & S, T are_homeomorphic
  holds T is injective;

theorem :: WAYBEL25:7
   for L1, L2 being complete LATTICE,
     T1 being Scott TopAugmentation of L1,
     T2 being Scott TopAugmentation of L2 st L1, L2 are_isomorphic &
     T1 is injective holds
  T2 is injective;

definition let X, Y be non empty TopSpace;
 redefine pred X is_Retract_of Y means
:: WAYBEL25:def 1
  ex c being continuous map of X, Y,
     r being continuous map of Y, X st r * c = id X;
end;

theorem :: WAYBEL25:8
 for S, T, X, Y being non empty TopSpace st
   the TopStruct of S = the TopStruct of T &
   the TopStruct of X = the TopStruct of Y &
   S is_Retract_of X holds
  T is_Retract_of Y;

theorem :: WAYBEL25:9
   for T, S1, S2 being non empty TopStruct st S1, S2 are_homeomorphic &
  S1 is_Retract_of T holds S2 is_Retract_of T;

theorem :: WAYBEL25:10
   for S, T being non empty TopSpace st T is injective & S is_Retract_of T
  holds S is injective;

::p.126 exercise 3.13, 1 => 2
theorem :: WAYBEL25:11
   for J being injective non empty TopSpace, Y being non empty TopSpace st
  J is SubSpace of Y holds J is_Retract_of Y;

:: p.123 proposition 3.5
:: p.124 theorem 3.8 (i, part a)
:: p.126 exercise 3.14
theorem :: WAYBEL25:12
 for L being complete continuous LATTICE, T being Scott TopAugmentation of L
  holds T is injective;

definition let L be complete continuous LATTICE;
 cluster Scott -> injective TopAugmentation of L;
end;

definition let T be injective non empty TopSpace;
 cluster the TopStruct of T -> injective;
end;

begin  :: Specialization order

::p.124 definition 3.6
definition let T be TopStruct;
 func Omega T -> strict TopRelStr means
:: WAYBEL25:def 2
  the TopStruct of it = the TopStruct of T &
  for x, y being Element of it holds x <= y iff
    ex Y being Subset of T st Y = {y} & x in Cl Y;
end;

definition let T be empty TopStruct;
 cluster Omega T -> empty;
end;

definition let T be non empty TopStruct;
 cluster Omega T -> non empty;
end;

definition let T be TopSpace;
 cluster Omega T -> TopSpace-like;
end;

definition let T be TopStruct;
 cluster Omega T -> reflexive;
end;

definition let T be TopStruct;
 cluster Omega T -> transitive;
end;

definition let T be T_0-TopSpace;
 cluster Omega T -> antisymmetric;
end;

theorem :: WAYBEL25:13
 for S, T being TopSpace st the TopStruct of S = the TopStruct of T
  holds Omega S = Omega T;

theorem :: WAYBEL25:14
   for M being non empty set, T being non empty TopSpace holds
  the RelStr of Omega product(M --> T) = the RelStr of product(M --> Omega T);

::p.124 theorem 3.8 (i, part b)
theorem :: WAYBEL25:15
 for S being Scott complete TopLattice holds Omega S = the TopRelStr of S;

::p.124 theorem 3.8 (i, part b)
theorem :: WAYBEL25:16
 for L being complete LATTICE,
     S being Scott TopAugmentation of L holds
  the RelStr of Omega S = the RelStr of L;

definition let S be Scott complete TopLattice;
 cluster Omega S -> complete;
end;

theorem :: WAYBEL25:17
 for T being non empty TopSpace, S being non empty SubSpace of T holds
  Omega S is full SubRelStr of Omega T;

theorem :: WAYBEL25:18
 for S, T being TopSpace, h being map of S, T, g being map of Omega S, Omega T
  st h = g & h is_homeomorphism holds g is isomorphic;

theorem :: WAYBEL25:19
 for S, T being TopSpace st S, T are_homeomorphic holds
  Omega S, Omega T are_isomorphic;

::p.124 proposition 3.7
::p.124 theorem 3.8 (ii, part a)
theorem :: WAYBEL25:20
 for T being injective T_0-TopSpace holds
  Omega T is complete continuous LATTICE;

definition let T be injective T_0-TopSpace;
 cluster Omega T -> complete continuous;
end;

theorem :: WAYBEL25:21
 for X, Y being non empty TopSpace,
     f being continuous map of Omega X, Omega Y holds
  f is monotone;

definition let X, Y be non empty TopSpace;
 cluster continuous -> monotone map of Omega X, Omega Y;
end;

theorem :: WAYBEL25:22
 for T being non empty TopSpace, x being Element of Omega T
  holds Cl {x} = downarrow x;

definition let T be non empty TopSpace,
               x be Element of Omega T;
 cluster Cl {x} -> non empty lower directed;
 cluster downarrow x -> closed;
end;

theorem :: WAYBEL25:23
 for X being TopSpace, A being open Subset of Omega X holds A is upper;

definition let T be TopSpace;
 cluster open -> upper Subset of Omega T;
end;

definition let I be non empty set,
               S, T be non empty RelStr,
               N be net of T,
               i be Element of I such that
 the carrier of T c= the carrier of S |^ I;
 func commute(N,i,S) -> strict net of S means
:: WAYBEL25:def 3
  the RelStr of it = the RelStr of N &
  the mapping of it = (commute the mapping of N).i;
end;

theorem :: WAYBEL25:24
 for X, Y being non empty TopSpace,
     N being net of ContMaps(X,Omega Y),
     i being Element of N,
     x being Point of X holds
  (the mapping of commute(N,x,Omega Y)).i = (the mapping of N).i.x;

theorem :: WAYBEL25:25
 for X, Y being non empty TopSpace,
     N being eventually-directed net of ContMaps(X,Omega Y),
     x being Point of X holds
  commute(N,x,Omega Y) is eventually-directed;

definition let X, Y be non empty TopSpace,
               N be eventually-directed net of ContMaps(X,Omega Y),
               x be Point of X;
 cluster commute(N,x,Omega Y) -> eventually-directed;
end;

definition let X, Y be non empty TopSpace;
 cluster -> Function-yielding net of ContMaps(X,Omega Y);
end;

theorem :: WAYBEL25:26
 for X being non empty TopSpace,
     Y being T_0-TopSpace,
     N being net of ContMaps(X,Omega Y) st
   for x being Point of X holds ex_sup_of commute(N,x,Omega Y)
 holds ex_sup_of rng the mapping of N, (Omega Y) |^ the carrier of X;

begin  :: Monotone convergence topological spaces

::p.125 definition 3.9
definition let T be non empty TopSpace;
 attr T is monotone-convergence means
:: WAYBEL25:def 4
  for D being non empty directed Subset of Omega T holds ex_sup_of D,Omega T &
   for V being open Subset of T st sup D in V holds D meets V;
end;

theorem :: WAYBEL25:27
 for S, T being non empty TopSpace st
  the TopStruct of S = the TopStruct of T & S is monotone-convergence holds
 T is monotone-convergence;

definition
 cluster trivial -> monotone-convergence T_0-TopSpace;
end;

definition
 cluster strict trivial non empty TopSpace;
end;

theorem :: WAYBEL25:28
   for S being monotone-convergence T_0-TopSpace,
     T being T_0-TopSpace st S, T are_homeomorphic holds
   T is monotone-convergence;

theorem :: WAYBEL25:29
 for S being Scott complete TopLattice holds S is monotone-convergence;

definition let L be complete LATTICE;
 cluster -> monotone-convergence (Scott TopAugmentation of L);
end;

definition let L be complete LATTICE,
               S be Scott TopAugmentation of L;
 cluster the TopStruct of S -> monotone-convergence;
end;

theorem :: WAYBEL25:30
 for X being monotone-convergence T_0-TopSpace holds Omega X is up-complete;

definition let X be monotone-convergence T_0-TopSpace;
 cluster Omega X -> up-complete;
end;

theorem :: WAYBEL25:31
 for X being monotone-convergence (non empty TopSpace),
     N being eventually-directed prenet of Omega X holds ex_sup_of N;

theorem :: WAYBEL25:32
 for X being monotone-convergence (non empty TopSpace),
     N being eventually-directed net of Omega X holds sup N in Lim N;

theorem :: WAYBEL25:33
 for X being monotone-convergence (non empty TopSpace),
     N being eventually-directed net of Omega X holds
  N is convergent;

definition let X be monotone-convergence (non empty TopSpace);
 cluster -> convergent (eventually-directed net of Omega X);
end;

theorem :: WAYBEL25:34
   for X being non empty TopSpace st
  for N being eventually-directed net of Omega X holds
   ex_sup_of N & sup N in Lim N
 holds X is monotone-convergence;

::p.125 lemma 3.10
theorem :: WAYBEL25:35
 for X being monotone-convergence (non empty TopSpace),
     Y being T_0-TopSpace,
     f being continuous map of Omega X, Omega Y holds
  f is directed-sups-preserving;

definition let X be monotone-convergence (non empty TopSpace),
               Y be T_0-TopSpace;
 cluster continuous -> directed-sups-preserving map of Omega X, Omega Y;
end;

theorem :: WAYBEL25:36
 for T being monotone-convergence T_0-TopSpace,
     R being T_0-TopSpace st R is_Retract_of T holds
  R is monotone-convergence;

::p.124 theorem 3.8 (ii, part b)
theorem :: WAYBEL25:37
 for T being injective T_0-TopSpace, S being Scott TopAugmentation of Omega T
  holds the TopStruct of S = the TopStruct of T;

theorem :: WAYBEL25:38
   for T being injective T_0-TopSpace holds T is compact locally-compact sober;

theorem :: WAYBEL25:39
 for T being injective T_0-TopSpace holds T is monotone-convergence;

definition
 cluster injective -> monotone-convergence T_0-TopSpace;
end;

theorem :: WAYBEL25:40
 for X being non empty TopSpace,
     Y being monotone-convergence T_0-TopSpace,
     N being net of ContMaps(X,Omega Y),
     f, g being map of X, Omega Y
   st f = "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X) &
      ex_sup_of rng the mapping of N, (Omega Y) |^ the carrier of X &
      g in rng the mapping of N holds
  g <= f;

theorem :: WAYBEL25:41
 for X being non empty TopSpace,
     Y being monotone-convergence T_0-TopSpace,
     N being net of ContMaps(X,Omega Y),
     x being Point of X,
     f being map of X, Omega Y st
   (for a being Point of X holds commute(N,a,Omega Y) is eventually-directed) &
   f = "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X)
  holds f.x = sup commute(N,x,Omega Y);

::p.125 lemma 3.11
theorem :: WAYBEL25:42
 for X being non empty TopSpace,
     Y being monotone-convergence T_0-TopSpace,
     N being net of ContMaps(X,Omega Y) st
   for x being Point of X holds commute(N,x,Omega Y) is eventually-directed
     holds
  "\/"(rng the mapping of N, (Omega Y) |^ the carrier of X)
   is continuous map of X, Y;

::p.126 lemma 3.12 (i)
theorem :: WAYBEL25:43
   for X being non empty TopSpace,
     Y being monotone-convergence T_0-TopSpace holds
  ContMaps(X,Omega Y) is directed-sups-inheriting
   SubRelStr of (Omega Y) |^ the carrier of X;