The abstract of the Mizar article:

Injective Spaces

by

Jaroslaw Gryko

Received April 17, 1998

MML identifier: WAYBEL18

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, FUNCT_1, RELAT_1, SETFAM_1, CANTOR_1, TARSKI, PRE_TOPC,
      PRALG_1, PBOOLE, FUNCOP_1, WAYBEL_3, CARD_3, RLVECT_2, FUNCT_4, BORSUK_1,
      ORDINAL2, FUNCTOR0, PARTFUN1, FUNCT_6, FUNCT_3, GROUP_6, SUBSET_1,
      WAYBEL_1, SGRAPH1, T_0TOPSP, TOPS_2, METRIC_1, RELAT_2, ORDERS_1,
      WAYBEL11, YELLOW_9, YELLOW_1, LATTICE3, FILTER_1, WAYBEL_0, QUANTAL1,
      YELLOW_0, FINSET_1, BHSP_3, WAYBEL_8, LATTICES, CAT_1, WAYBEL_9,
      COMPTS_1, WAYBEL18, RLVECT_3;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
      T_0TOPSP, STRUCT_0, FUNCT_1, FUNCT_2, PRE_TOPC, FUNCT_3, FUNCT_6,
      FUNCT_7, PBOOLE, CARD_3, PRALG_1, ORDERS_1, LATTICE3, YELLOW_1, PRE_CIRC,
      CANTOR_1, FINSET_1, PRALG_3, TOPS_2, BORSUK_1, TMAP_1, GRCAT_1, YELLOW_0,
      YELLOW_2, YELLOW_9, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11;
 constructors PRALG_3, CANTOR_1, WAYBEL_1, WAYBEL_3, ENUMSET1, T_0TOPSP,
      GRCAT_1, TOPS_2, FUNCT_7, WAYBEL_8, WAYBEL11, TMAP_1, WAYBEL_5, YELLOW_9,
      LATTICE3, BORSUK_1;
 clusters STRUCT_0, PRE_TOPC, FUNCT_1, LATTICE3, YELLOW_1, WAYBEL_0, WAYBEL_3,
      WAYBEL_8, WAYBEL11, YELLOW_9, FUNCOP_1, RELSET_1, SUBSET_1, BORSUK_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

theorem :: WAYBEL18:1
 for x,y,z,Z being set holds
  Z c= {x,y,z} iff Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or
                   Z = {y,z} or Z = {x,z} or Z = {x,y,z};

theorem :: WAYBEL18:2
for X being set, A,B being Subset-Family of X st B = A \ {{}} or A = B \/ {{}}
 holds UniCl A = UniCl B;

theorem :: WAYBEL18:3
for T being TopSpace, K being Subset-Family of T
  holds K is Basis of T iff K \ {{}} is Basis of T;

definition let F be Relation;
 attr F is TopSpace-yielding means
:: WAYBEL18:def 1
 for x being set st x in rng F holds x is TopStruct;
end;

definition
 cluster TopSpace-yielding -> 1-sorted-yielding Function;
end;

definition let I be set;
 cluster TopSpace-yielding ManySortedSet of I;
end;

definition let I be set;
 cluster TopSpace-yielding non-Empty ManySortedSet of I;
end;

definition let J be non empty set;
           let A be TopSpace-yielding ManySortedSet of J;
           let j be Element of J;
 redefine func A.j -> TopStruct;
end;

definition let I be set; let J be TopSpace-yielding ManySortedSet of I;
 func product_prebasis J -> Subset-Family of product Carrier J means
:: WAYBEL18:def 2
 for x being Subset of product Carrier J holds
  x in it iff ex i being set, T being TopStruct,
       V being Subset of T st i in I &
       V is open & T = J.i & x = product ((Carrier J) +* (i,V));
end;

theorem :: WAYBEL18:4
 for X be set, A be Subset-Family of X holds
  TopStruct (#X,UniCl FinMeetCl A#) is TopSpace-like;

definition let I be set;
           let J be TopSpace-yielding non-Empty ManySortedSet of I;
 func product J -> strict TopSpace means
:: WAYBEL18:def 3
  the carrier of it = product Carrier J &
  product_prebasis J is prebasis of it;
end;

definition let I be set;
           let J be TopSpace-yielding non-Empty ManySortedSet of I;
 cluster product J -> non empty;
end;

definition let I be non empty set;
           let J be TopSpace-yielding non-Empty ManySortedSet of I;
           let i be Element of I;
redefine func J.i -> non empty TopStruct;
end;

definition let I be set;
           let J be TopSpace-yielding non-Empty ManySortedSet of I;
 cluster -> Function-like Relation-like Element of product J;
end;

definition
 let I be non empty set;
 let J be TopSpace-yielding non-Empty ManySortedSet of I;
 let x be Element of product J; let i be Element of I;
 redefine func x.i -> Element of J.i;
end;

definition let I be non empty set;
           let J be TopSpace-yielding non-Empty ManySortedSet of I;
           let i be Element of I;
 func proj(J,i) -> map of product J, J.i equals
:: WAYBEL18:def 4
   proj(Carrier J,i);
end;

theorem :: WAYBEL18:5
for I being non empty set,
    J being TopSpace-yielding non-Empty ManySortedSet of I,
    i being Element of I, P being Subset of J.i holds
 proj(J,i)"P = product ((Carrier J) +* (i,P));

theorem :: WAYBEL18:6
for I being non empty set,
 J being TopSpace-yielding non-Empty ManySortedSet of I,
 i being Element of I holds proj(J,i) is continuous;

theorem :: WAYBEL18:7
for X being non empty TopSpace, I being non empty set,
 J being TopSpace-yielding non-Empty ManySortedSet of I,
 f being map of X, product J holds
    f is continuous iff
    for i being Element of I holds proj(J,i)*f is continuous;

begin :: Main Part

definition let Z be TopStruct;
 attr Z is injective means
:: WAYBEL18:def 5    ::p.121 definition 3.1.
 for X being non empty TopSpace
  for f being map of X, Z st f is continuous holds
  for Y being non empty TopSpace st X is SubSpace of Y
   ex g being map of Y,Z st g is continuous & g|(the carrier of X) = f;
end;

theorem :: WAYBEL18:8   ::p.121 lemma 3.2.(i)
for I being non empty set, J being TopSpace-yielding non-Empty
 ManySortedSet of I st for i being Element of I holds J.i is injective holds
 product J is injective;

theorem :: WAYBEL18:9       ::p.121 lemma 3.2.(ii)
   for T being non empty TopSpace st T is injective
  for S being non empty SubSpace of T st S is_a_retract_of T holds
   S is injective;

definition let X be 1-sorted, Y be TopStruct, f be map of X,Y;
 func Image f -> SubSpace of Y equals
:: WAYBEL18:def 6
  Y|(rng f);
end;

definition let X be non empty 1-sorted,
               Y be non empty TopStruct,
               f be map of X,Y;
 cluster Image f -> non empty;
end;

theorem :: WAYBEL18:10
 for X being 1-sorted, Y being TopStruct,
     f being map of X,Y holds
 the carrier of Image f = rng f;

definition let X be 1-sorted, Y be non empty TopStruct,
               f be map of X,Y;
 func corestr(f) -> map of X,Image f equals
:: WAYBEL18:def 7
   f;
end;

theorem :: WAYBEL18:11
for X, Y being non empty TopSpace, f being map of X,Y st
  f is continuous holds
 corestr f is continuous;

definition let X be 1-sorted,Y be non empty TopStruct; let f be map of X,Y;
 cluster corestr f -> onto;
end;

definition let X,Y be TopStruct;
 pred X is_Retract_of Y means
:: WAYBEL18:def 8
   ex f being map of Y,Y st f is continuous & f*f = f &
  Image f, X are_homeomorphic;
end;

theorem :: WAYBEL18:12   ::p.121 lemma 3.2.(iii)
for T,S being non empty TopSpace st T is injective
 for f being map of T,S st corestr(f) is_homeomorphism holds
  T is_Retract_of S;

definition
 func Sierpinski_Space -> strict TopStruct means
:: WAYBEL18:def 9
  the carrier of it = {0,1} &
  the topology of it = {{}, {1}, {0,1} };
end;

definition
 cluster Sierpinski_Space -> non empty TopSpace-like;
end;

definition
 cluster Sierpinski_Space -> discerning;
end;

definition       ::p.122 lemma 3.3.
 cluster Sierpinski_Space -> injective;
end;

definition let I be set; let S be non empty 1-sorted;
 cluster I --> S -> non-Empty;
end;

definition let I be set; let T be TopStruct;
 cluster I --> T -> TopSpace-yielding;
end;

definition let I be set; let L be reflexive RelStr;
 cluster I --> L -> reflexive-yielding;
end;

definition let I be non empty set; let L be non empty antisymmetric RelStr;
 cluster product (I --> L) -> antisymmetric;
end;

definition let I be non empty set; let L be non empty transitive RelStr;
 cluster product (I --> L) -> transitive;
end;

theorem :: WAYBEL18:13
  for T being Scott TopAugmentation of BoolePoset 1
 holds the topology of T = the topology of Sierpinski_Space;

theorem :: WAYBEL18:14
 for I being non empty set holds
   {product ((Carrier (I --> Sierpinski_Space))+*(i,{1}))
        where i is Element of I: not contradiction }
   is prebasis of product (I --> Sierpinski_Space);

definition let I be non empty set; let L be complete LATTICE;
 cluster product (I --> L) -> with_suprema complete;
end;

definition let I be non empty set; let X be algebraic lower-bounded LATTICE;
 cluster product (I --> X) -> algebraic;
end;

theorem :: WAYBEL18:15
 for X being non empty set
  ex f being map of BoolePoset X, product (X --> BoolePoset 1) st
  f is isomorphic & for Y being Subset of X holds f.Y = chi(Y,X);

theorem :: WAYBEL18:16   ::p.122 lemma 3.4.(i)
for I being non empty set
 for T being Scott TopAugmentation of product (I --> BoolePoset 1) holds
  the topology of T = the topology of product (I --> Sierpinski_Space);

theorem :: WAYBEL18:17
for T,S being non empty TopSpace st the carrier of T = the carrier of S &
 the topology of T = the topology of S & T is injective holds S is injective;

theorem :: WAYBEL18:18       ::p.122 lemma 3.4.(i) part II
  for I being non empty set
 for T being Scott TopAugmentation of product (I --> BoolePoset 1)
  holds T is injective;

theorem :: WAYBEL18:19   ::p.122 lemma 3.4.(ii)
for T being T_0-TopSpace ex M being non empty set,
 f being map of T, product (M --> Sierpinski_Space) st
  corestr(f) is_homeomorphism;

theorem :: WAYBEL18:20       ::p.122 lemma 3.4.(iii)
  for T being T_0-TopSpace st T is injective ex M being non empty set st
 T is_Retract_of product (M --> Sierpinski_Space);