:: 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 b₁ being Function st b₁ is TopStruct-yielding holds
b₁ 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 b₁ being ManySortedSet of I st b₁ 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 b₁ being ManySortedSet of I st
( b₁ is TopStruct-yielding & b₁ 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 b₁ being Subset-Family of (product (Carrier J)) st
for x being Subset of (product (Carrier J)) holds
( x in b₁ 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 b₁, b₂ being Subset-Family of (product (Carrier J)) st ( for x being Subset of (product (Carrier J)) holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :
for I being set
for J being TopStruct-yielding ManySortedSet of I
for b₃ being Subset-Family of (product (Carrier J)) holds
( b₃ = product_prebasis J iff for x being Subset of (product (Carrier J)) holds
( x in b₃ 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 b₁ being strict TopSpace st
( the carrier of b₁ = product (Carrier J) & product_prebasis J is prebasis of b₁ )

proof end;

uniqueness
for b₁, b₂ being strict TopSpace st the carrier of b₁ = product (Carrier J) & product_prebasis J is prebasis of b₁ & the carrier of b₂ = product (Carrier J) & product_prebasis J is prebasis of b₂ holds
b₁ = b₂

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 b₃ being strict TopSpace holds
( b₃ = product J iff ( the carrier of b₃ = product (Carrier J) & product_prebasis J is prebasis of b₃ ) );

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 b₁ being strict TopStruct st
( the carrier of b₁ = {0,1} & the topology of b₁ = {{},{1},{0,1}} )

proof end;

uniqueness
for b₁, b₂ being strict TopStruct st the carrier of b₁ = {0,1} & the topology of b₁ = {{},{1},{0,1}} & the carrier of b₂ = {0,1} & the topology of b₂ = {{},{1},{0,1}} holds
b₁ = b₂ ;

end;

:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def 9 :
for b₁ being strict TopStruct holds
( b₁ = Sierpinski_Space iff ( the carrier of b₁ = {0,1} & the topology of b₁ = {{},{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;