Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### 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);

Back to top