:: Injective Spaces
:: by Jaros{\l}aw Gryko
::
:: Received April 17, 1998
:: Copyright (c) 1998-2017 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,
CARD_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 set 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);