:: Injective Spaces, Part { II }
::  by Artur Korni{\l}owicz and Jaros{\l}aw Gryko
::
:: Received July 3, 1999
:: Copyright (c) 1999-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 PRE_TOPC, WAYBEL18, CARD_1, RCOMP_1, STRUCT_0, SUBSET_1,
      XBOOLE_0, TARSKI, REWRITE1, WAYBEL11, WAYBEL_9, FUNCTOR0, T_0TOPSP,
      YELLOW_9, CARD_3, FUNCOP_1, YELLOW_1, RELAT_1, RLVECT_2, FUNCT_1,
      ZFMISC_1, ORDERS_2, WAYBEL_0, CAT_1, TOPS_2, WELLORD1, ORDINAL2, GROUP_6,
      WAYBEL_1, FUNCT_3, BORSUK_1, EQREL_1, XXREAL_0, LATTICE3, YELLOW_0,
      WAYBEL_3, RELAT_2, PROB_1, BINOP_1, SEQM_3, WAYBEL24, FUNCT_2, NEWTON,
      FUNCT_6, YELLOW_2, ORDINAL1, CONNSP_2, TOPS_1, SEQ_2, YELLOW_8, SETFAM_1,
      WAYBEL25;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCT_3, NATTRA_1,
      TOLER_1, QUANTAL1, CARD_3, PRALG_1, FUNCT_6, FUNCOP_1, WAYBEL18,
      DOMAIN_1, STRUCT_0, PRE_TOPC, CONNSP_2, TOPS_1, TOPS_2, COMPTS_1,
      BORSUK_1, TMAP_1, T_0TOPSP, BORSUK_3, ORDERS_2, 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 TOLER_1, FUNCT_6, TOPS_1, TOPS_2, NATTRA_1, BORSUK_1, TMAP_1,
      CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_8, YELLOW_8,
      WAYBEL17, YELLOW_9, BORSUK_3, WAYBEL24, YELLOW14, COMPTS_1, WAYBEL_2;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
      STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TEX_1, TSP_1,
      BORSUK_2, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8,
      WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL19, WAYBEL21, WAYBEL24,
      YELLOW14, RELSET_1;
 requirements SUBSET, BOOLE, NUMERALS;


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;

registration
  cluster Sierpinski_Space -> non T_1;
end;

registration
  cluster complete Scott -> T_0 for TopLattice;
end;

registration
  cluster injective strict for T_0-TopSpace;
end;

registration
  cluster complete Scott strict for TopLattice;
end;

theorem :: WAYBEL25:3  :: see WAYBEL18:16
  for I being non empty set, T being Scott TopAugmentation of
  product(I --> BoolePoset{0})
   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 Function of L1, L2, H
  being Function of T1, T2 st h = H & h is isomorphic holds H is
  being_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 Function
  of X, Y, r being continuous Function 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;

theorem :: WAYBEL25:11 ::p.126 exercise 3.13, 1 => 2
  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;

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

registration
  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;

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

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

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

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

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

registration
  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;

registration
  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 Function of S, T, g being
  Function of Omega S, Omega T st h = g & h is being_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;

registration
  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 Function
  of Omega X, Omega Y holds f is monotone;

registration
  let X, Y be non empty TopSpace;
  cluster continuous -> monotone for Function 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;

registration
  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;

registration
  let T be TopSpace;
  cluster open -> upper for 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;

registration
  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;

registration
  let X, Y be non empty TopSpace;
  cluster -> Function-yielding for 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;

registration
  cluster trivial -> monotone-convergence for T_0-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;

registration
  let L be complete LATTICE;
  cluster -> monotone-convergence for Scott TopAugmentation of L;
end;

registration
  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;

registration
  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;

registration
  let X be monotone-convergence non empty TopSpace;
  cluster -> convergent for 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 Function of Omega X, Omega Y holds f is
  directed-sups-preserving;

registration
  let X be monotone-convergence non empty TopSpace, Y be T_0-TopSpace;
  cluster continuous -> directed-sups-preserving for
Function 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;

registration
  cluster injective -> monotone-convergence for 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 Function 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
Function 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 Function 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;