:: WAYBEL18 semantic presentation

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} ) )

proof end;

Lm1: for X being set
for f, g being Function holds f " (g " X) = (g * f) " X

proof end;

theorem Th2: :: WAYBEL18:2

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 Th3: :: WAYBEL18:3

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 TopSpace-yielding means :Def1: :: WAYBEL18:def 1
for x being set st x in rng F holds
x is TopStruct ;

end;

:: deftheorem Def1 defines TopSpace-yielding WAYBEL18:def 1 :

registration

cluster TopSpace-yielding -> 1-sorted-yielding set ;
coherence

proof end;

end;

registration

let I be set ;
cluster 1-sorted-yielding TopSpace-yielding ManySortedSet of I;
existence

proof end;

end;

registration

let I be set ;
cluster non-Empty 1-sorted-yielding TopSpace-yielding ManySortedSet of I;
existence

proof end;

end;

definition

let J be non empty set ;
let A be TopSpace-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine func A . j -> TopStruct ;
coherence

proof end;

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 :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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :

theorem Th4: :: WAYBEL18:4

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 TopSpace-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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines product WAYBEL18:def 3 :

registration

let I be set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
cluster product J -> non empty strict ;
coherence

proof end;

end;

definition

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

proof end;

end;

registration

let I be set ;
let J be non-Empty TopSpace-yielding ManySortedSet of I;
cluster product J -> non empty strict constituted-Functions ;
coherence

proof end;

end;

definition

let I be non empty set ;
let J be non-Empty TopSpace-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

proof end;

end;

definition

let I be non empty set ;
let J be non-Empty TopSpace-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

proof end;

end;

:: deftheorem defines proj WAYBEL18:def 4 :

theorem Th5: :: WAYBEL18:5

for I being non empty set
for J being non-Empty TopSpace-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 Th6: :: WAYBEL18:6

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds proj J,i is continuous

proof end;

theorem Th7: :: WAYBEL18:7

for X being non empty TopSpace
for I being non empty set
for J being non-Empty TopSpace-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 :Def5: :: 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 Def5 defines injective WAYBEL18:def 5 :

theorem Th8: :: WAYBEL18:8

for I being non empty set
for J being non-Empty TopSpace-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:9

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 ;

end;

:: deftheorem defines Image WAYBEL18:def 6 :

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

proof end;

end;

theorem Th10: :: WAYBEL18:10

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

proof end;

end;

:: deftheorem defines corestr WAYBEL18:def 7 :

theorem Th11: :: WAYBEL18:11

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

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 :

theorem Th12: :: WAYBEL18:12

for T, S being non empty TopSpace st T is injective holds
for f being Function of T,S st corestr f is_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

proof end;

uniqueness ;

end;

:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def 9 :

registration

cluster Sierpinski_Space -> non empty strict TopSpace-like ;
coherence

proof end;

end;

Lm2: Sierpinski_Space is discerning

proof end;

registration

cluster Sierpinski_Space -> non empty strict TopSpace-like discerning ;
coherence by Lm2;

end;

registration

cluster Sierpinski_Space -> non empty strict TopSpace-like discerning injective ;
coherence

proof end;

end;

registration

let I be set ;
let S be non empty 1-sorted ;
cluster I --> S -> non-Empty ;
coherence

proof end;

end;

registration

let I be set ;
let T be TopStruct ;
cluster I --> T -> 1-sorted-yielding TopSpace-yielding ;
coherence

proof end;

end;

registration

let I be set ;
let L be reflexive RelStr ;
cluster I --> L -> reflexive-yielding ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem :: WAYBEL18:13

for T being Scott TopAugmentation of BoolePoset 1 holds the topology of T = the topology of Sierpinski_Space

proof end;

theorem Th14: :: WAYBEL18:14

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) -> transitive antisymmetric with_suprema complete ;
coherence

proof end;

end;

registration

let I be non empty set ;
let X be lower-bounded algebraic LATTICE;
cluster product (I --> X) -> transitive antisymmetric algebraic with_suprema complete ;
coherence

proof end;

end;

theorem Th15: :: WAYBEL18:15

for X being non empty set ex f being Function of (BoolePoset X),(product (X --> (BoolePoset 1))) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi Y,X ) )

proof end;

theorem Th16: :: WAYBEL18:16

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

proof end;

theorem Th17: :: 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

proof end;

theorem :: WAYBEL18:18

for I being non empty set
for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds T is injective

proof end;

theorem Th19: :: WAYBEL18:19

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_homeomorphism

proof end;

theorem :: WAYBEL18:20

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;