:: Injective Spaces
:: by Jaros{\l}aw Gryko
::
:: Received April 17, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users


theorem Th1: :: WAYBEL18:1
for X being set
for A, B being Subset-Family of X st ( B = A \ {{}} or A = B \/ {{}} ) holds
UniCl A = UniCl B
proof end;

theorem Th2: :: WAYBEL18:2
for T being TopSpace
for K being Subset-Family of T holds
( K is Basis of T iff K \ {{}} is Basis of T )
proof end;

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

:: deftheorem Def1 defines TopStruct-yielding WAYBEL18:def 1 :
for F being Relation holds
( F is TopStruct-yielding iff for x being object st x in rng F holds
x is TopStruct );

registration
cluster Relation-like Function-like TopStruct-yielding -> 1-sorted-yielding for set ;
coherence
for b1 being Function st b1 is TopStruct-yielding holds
b1 is 1-sorted-yielding
proof end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total TopStruct-yielding for set ;
existence
ex b1 being ManySortedSet of I st b1 is TopStruct-yielding
proof end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like total non-Empty TopStruct-yielding for set ;
existence
ex b1 being ManySortedSet of I st
( b1 is TopStruct-yielding & b1 is non-Empty )
proof end;
end;

definition
let J be non empty set ;
let A be TopStruct-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine func A . j -> TopStruct ;
coherence
A . j is TopStruct
proof end;
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 :Def2: :: WAYBEL18:def 2
for x being Subset of (product (Carrier J)) holds
( x in it iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) );
existence
ex b1 being Subset-Family of (product (Carrier J)) st
for x being Subset of (product (Carrier J)) holds
( x in b1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of (product (Carrier J)) st ( for x being Subset of (product (Carrier J)) holds
( x in b1 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) & ( for x being Subset of (product (Carrier J)) holds
( x in b2 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :
for I being set
for J being TopStruct-yielding ManySortedSet of I
for b3 being Subset-Family of (product (Carrier J)) holds
( b3 = product_prebasis J iff for x being Subset of (product (Carrier J)) holds
( x in b3 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) );

theorem Th3: :: WAYBEL18:3
for X being set
for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
proof end;

definition
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
func product J -> strict TopSpace means :Def3: :: WAYBEL18:def 3
( the carrier of it = product (Carrier J) & product_prebasis J is prebasis of it );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = product (Carrier J) & product_prebasis J is prebasis of b1 )
proof end;
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = product (Carrier J) & product_prebasis J is prebasis of b1 & the carrier of b2 = product (Carrier J) & product_prebasis J is prebasis of b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines product WAYBEL18:def 3 :
for I being set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for b3 being strict TopSpace holds
( b3 = product J iff ( the carrier of b3 = product (Carrier J) & product_prebasis J is prebasis of b3 ) );

registration
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
cluster product J -> non empty strict ;
coherence
not product J is empty
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func J . i -> non empty TopStruct ;
coherence
J . i is non empty TopStruct
proof end;
end;

registration
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
cluster product J -> strict constituted-Functions ;
coherence
product J is constituted-Functions
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
let x be Element of (product J);
let i be Element of I;
:: original: .
redefine func x . i -> Element of (J . i);
coherence
x . i is Element of (J . i)
proof end;
end;

definition
let I be non empty set ;
let J be non-Empty TopStruct-yielding 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);
coherence
proj ((Carrier J),i) is Function of (product J),(J . i)
proof end;
end;

:: deftheorem defines proj WAYBEL18:def 4 :
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) = proj ((Carrier J),i);

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

theorem Th5: :: WAYBEL18:5
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) is continuous
proof end;

theorem Th6: :: WAYBEL18:6
for X being non empty TopSpace
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for 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 )
proof end;

definition
let Z be TopStruct ;
attr Z is injective means :: WAYBEL18:def 5
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 holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f );
end;

:: deftheorem defines injective WAYBEL18:def 5 :
for Z being TopStruct holds
( Z is injective iff 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 holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f ) );

theorem Th7: :: WAYBEL18:7
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds
product J is injective
proof end;

theorem :: WAYBEL18:8
for T being non empty TopSpace st T is injective holds
for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective
proof end;

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

:: deftheorem defines Image WAYBEL18:def 6 :
for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds Image f = Y | (rng f);

registration
let X be non empty 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
cluster Image f -> non empty ;
coherence
not Image f is empty
;
end;

theorem Th9: :: WAYBEL18:9
for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds the carrier of (Image f) = rng f
proof end;

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

:: deftheorem defines corestr WAYBEL18:def 7 :
for X being 1-sorted
for Y being non empty TopStruct
for f being Function of X,Y holds corestr f = f;

theorem Th10: :: WAYBEL18:10
for X, Y being non empty TopSpace
for f being Function of X,Y st f is continuous holds
corestr f is continuous
proof end;

registration
let X be 1-sorted ;
let Y be non empty TopStruct ;
let f be Function of X,Y;
cluster corestr f -> onto ;
coherence
corestr f is onto
proof end;
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;

:: deftheorem defines is_Retract_of WAYBEL18:def 8 :
for X, Y being TopStruct holds
( X is_Retract_of Y iff ex f being Function of Y,Y st
( f is continuous & f * f = f & Image f,X are_homeomorphic ) );

theorem Th11: :: WAYBEL18:11
for T, S being non empty TopSpace st T is injective holds
for f being Function of T,S st corestr f is being_homeomorphism holds
T is_Retract_of S
proof end;

definition
func Sierpinski_Space -> strict TopStruct means :Def9: :: WAYBEL18:def 9
( the carrier of it = {0,1} & the topology of it = {{},{1},{0,1}} );
existence
ex b1 being strict TopStruct st
( the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} )
proof end;
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} & the carrier of b2 = {0,1} & the topology of b2 = {{},{1},{0,1}} holds
b1 = b2
;
end;

:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def 9 :
for b1 being strict TopStruct holds
( b1 = Sierpinski_Space iff ( the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} ) );

registration
cluster Sierpinski_Space -> non empty strict TopSpace-like ;
coherence
( not Sierpinski_Space is empty & Sierpinski_Space is TopSpace-like )
proof end;
end;

Lm1: Sierpinski_Space is T_0
proof end;

registration
cluster Sierpinski_Space -> strict T_0 ;
coherence
Sierpinski_Space is T_0
by Lm1;
end;

registration
cluster Sierpinski_Space -> strict injective ;
coherence
Sierpinski_Space is injective
proof end;
end;

registration
let I be set ;
let S be non empty 1-sorted ;
cluster I --> S -> non-Empty ;
coherence
I --> S is non-Empty
proof end;
end;

registration
let I be set ;
let T be TopStruct ;
cluster I --> T -> TopStruct-yielding ;
coherence
I --> T is TopStruct-yielding
proof end;
end;

registration
let I be non empty set ;
let L be non empty antisymmetric RelStr ;
cluster product (I --> L) -> antisymmetric ;
coherence
product (I --> L) is antisymmetric
proof end;
end;

registration
let I be non empty set ;
let L be non empty transitive RelStr ;
cluster product (I --> L) -> transitive ;
coherence
product (I --> L) is transitive
proof end;
end;

theorem :: WAYBEL18:12
for T being Scott TopAugmentation of BoolePoset {0} holds the topology of T = the topology of Sierpinski_Space
proof end;

theorem Th13: :: WAYBEL18:13
for I being non empty set holds { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum } is prebasis of (product (I --> Sierpinski_Space))
proof end;

registration
let I be non empty set ;
let L be complete LATTICE;
cluster product (I --> L) -> with_suprema complete ;
coherence
( product (I --> L) is with_suprema & product (I --> L) is complete )
proof end;
end;

registration
let I be non empty set ;
let X be lower-bounded algebraic LATTICE;
cluster product (I --> X) -> algebraic ;
coherence
product (I --> X) is algebraic
proof end;
end;

theorem Th14: :: 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) ) )
proof end;

theorem Th15: :: WAYBEL18:15
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))
proof end;

theorem Th16: :: 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
proof end;

theorem :: WAYBEL18:17
for I being non empty set
for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds T is injective
proof end;

theorem Th18: :: WAYBEL18:18
for T being T_0-TopSpace ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
proof end;

theorem :: WAYBEL18:19
for T being T_0-TopSpace st T is injective holds
ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space)
proof end;