:: Injective Spaces :: by Jaros{\l}aw Gryko :: :: Received April 17, 1998 :: Copyright (c) 1998-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 SETFAM_1, XBOOLE_0, CANTOR_1, TARSKI, PRE_TOPC, RLVECT_3, RELAT_1, PRALG_1, FUNCT_1, PBOOLE, FUNCOP_1, WAYBEL_3, STRUCT_0, SUBSET_1, CARD_3, RLVECT_2, RCOMP_1, FUNCT_4, MONOID_0, ORDINAL2, FUNCTOR0, PARTFUN1, FUNCT_6, BORSUK_1, FUNCT_3, GROUP_6, WAYBEL_1, FUNCT_2, T_0TOPSP, TOPS_2, CARD_1, ZFMISC_1, RELAT_2, ORDERS_2, WAYBEL11, YELLOW_9, YELLOW_1, LATTICE3, FILTER_1, XXREAL_0, WAYBEL_0, CARD_FIL, FINSET_1, REWRITE1, WAYBEL_8, LATTICES, CAT_1, WAYBEL_9, WAYBEL18; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, RELAT_1, PBOOLE, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, ORDINAL1, NUMBERS, STRUCT_0, PRE_TOPC, T_0TOPSP, FUNCT_3, FUNCT_6, FUNCT_7, CARD_3, FUNCOP_1, MONOID_0, PRALG_1, ORDERS_2, LATTICE3, YELLOW_1, CANTOR_1, FINSET_1, TOPS_2, BORSUK_1, TMAP_1, YELLOW_0, YELLOW_9, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11; constructors FUNCT_3, FUNCT_7, TOPS_2, BORSUK_1, LATTICE3, TMAP_1, T_0TOPSP, CANTOR_1, MONOID_0, PRALG_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL11, YELLOW_9, BINOP_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, STRUCT_0, PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, WAYBEL_3, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL17, RELAT_1; requirements SUBSET, BOOLE, NUMERALS; begin :: Preliminaries theorem :: WAYBEL18:1 for X being set, A,B being Subset-Family of X st B = A \ {{}} or A = B \/ {{}} holds UniCl A = UniCl B; theorem :: WAYBEL18:2 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 TopStruct-yielding means :: WAYBEL18:def 1 for x being object st x in rng F holds x is TopStruct; end; registration cluster TopStruct-yielding -> 1-sorted-yielding for Function; end; registration let I be set; cluster TopStruct-yielding for ManySortedSet of I; end; registration let I be set; cluster TopStruct-yielding non-Empty for ManySortedSet of I; end; definition let J be non empty set; let A be TopStruct-yielding ManySortedSet of J; let j be Element of J; redefine func A.j -> TopStruct; end; definition let I be set; let J be TopStruct-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:3 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 TopStruct-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; registration let I be set; let J be TopStruct-yielding non-Empty ManySortedSet of I; cluster product J -> non empty; end; definition let I be non empty set; let J be TopStruct-yielding non-Empty ManySortedSet of I; let i be Element of I; redefine func J.i -> non empty TopStruct; end; registration let I be set; let J be TopStruct-yielding non-Empty ManySortedSet of I; cluster product J -> constituted-Functions; end; definition let I be non empty set; let J be TopStruct-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 TopStruct-yielding non-Empty ManySortedSet of I; let i be Element of I; func proj(J,i) -> Function of product J, J.i equals :: WAYBEL18:def 4 proj(Carrier J,i); end; theorem :: WAYBEL18:4 for I being non empty set, J being TopStruct-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:5 for I being non empty set, J being TopStruct-yielding non-Empty ManySortedSet of I, i being Element of I holds proj(J,i) is continuous; theorem :: WAYBEL18:6 for X being non empty TopSpace, I being non empty set, J being TopStruct-yielding non-Empty ManySortedSet of I, f being Function 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 Function of X, Z st f is continuous holds for Y being non empty TopSpace st X is SubSpace of Y ex g being Function of Y,Z st g is continuous & g|(the carrier of X) = f; end; theorem :: WAYBEL18:7 ::p.121 lemma 3.2.(i) for I being non empty set, J being TopStruct-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:8 ::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 Function of X,Y; func Image f -> SubSpace of Y equals :: WAYBEL18:def 6 Y|(rng f); end; registration let X be non empty 1-sorted, Y be non empty TopStruct, f be Function of X,Y; cluster Image f -> non empty; end; theorem :: WAYBEL18:9 for X being 1-sorted, Y being TopStruct, f being Function of X,Y holds the carrier of Image f = rng f; definition let X be 1-sorted, Y be non empty TopStruct, f be Function of X,Y; func corestr(f) -> Function of X,Image f equals :: WAYBEL18:def 7 f; end; theorem :: WAYBEL18:10 for X, Y being non empty TopSpace, f being Function of X,Y st f is continuous holds corestr f is continuous; registration let X be 1-sorted,Y be non empty TopStruct; let f be Function 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 Function of Y,Y st f is continuous & f*f = f & Image f, X are_homeomorphic; end; theorem :: WAYBEL18:11 ::p.121 lemma 3.2.(iii) for T,S being non empty TopSpace st T is injective for f being Function of T,S st corestr(f) is being_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; registration cluster Sierpinski_Space -> non empty TopSpace-like; end; registration cluster Sierpinski_Space -> T_0; end; registration ::p.122 lemma 3.3. cluster Sierpinski_Space -> injective; end; registration let I be set; let S be non empty 1-sorted; cluster I --> S -> non-Empty; end; registration let I be set; let T be TopStruct; cluster I --> T -> TopStruct-yielding; end; registration let I be non empty set; let L be non empty antisymmetric RelStr; cluster product (I --> L) -> antisymmetric; end; registration let I be non empty set; let L be non empty transitive RelStr; cluster product (I --> L) -> transitive; end; theorem :: WAYBEL18:12 for T being Scott TopAugmentation of BoolePoset {0} holds the topology of T = the topology of Sierpinski_Space; theorem :: WAYBEL18:13 for I being non empty set holds the set of all product ((Carrier (I --> Sierpinski_Space))+*(i,{1})) where i is Element of I is prebasis of product (I --> Sierpinski_Space); registration let I be non empty set; let L be complete LATTICE; cluster product (I --> L) -> with_suprema complete; end; registration let I be non empty set; let X be algebraic lower-bounded LATTICE; cluster product (I --> X) -> algebraic; end; theorem :: WAYBEL18:14 for X being non empty set ex f being Function of BoolePoset X, product (X --> BoolePoset {0}) st f is isomorphic & for Y being Subset of X holds f.Y = chi(Y,X); theorem :: WAYBEL18:15 ::p.122 lemma 3.4.(i) for I being non empty set for T being Scott TopAugmentation of product (I --> BoolePoset {0}) holds the topology of T = the topology of product (I --> Sierpinski_Space); theorem :: WAYBEL18:16 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:17 ::p.122 lemma 3.4.(i) part II for I being non empty set for T being Scott TopAugmentation of product (I --> BoolePoset{0}) holds T is injective; theorem :: WAYBEL18:18 ::p.122 lemma 3.4.(ii) for T being T_0-TopSpace ex M being non empty set, f being Function of T, product (M --> Sierpinski_Space) st corestr(f) is being_homeomorphism; theorem :: WAYBEL18:19 ::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);