:: WAYBEL18 semantic presentation

theorem Th1: :: WAYBEL18:1

for b₁, b₂, b₃, b₄ being set holds
( b₄ c= {b₁,b₂,b₃} iff ( b₄ = {} or b₄ = {b₁} or b₄ = {b₂} or b₄ = {b₃} or b₄ = {b₁,b₂} or b₄ = {b₂,b₃} or b₄ = {b₁,b₃} or b₄ = {b₁,b₂,b₃} ) )

proof end;

Lemma2: for b₁ being set
for b₂, b₃ being Function holds b₂ " (b₃ " b₁) = (b₃ * b₂) " b₁

proof end;

theorem Th2: :: WAYBEL18:2

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st ( b₃ = b₂ \ {{} } or b₂ = b₃ \/ {{} } ) holds
UniCl b₂ = UniCl b₃

proof end;

theorem Th3: :: WAYBEL18:3

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ holds
( b₂ is Basis of b₁ iff b₂ \ {{} } is Basis of b₁ )

proof end;

definition

let c₁ be Relation;
attr a₁ is TopSpace-yielding means :Def1: :: WAYBEL18:def 1
for b₁ being set st b₁ in rng a₁ holds
b₁ 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 c₁ be set ;
cluster 1-sorted-yielding TopSpace-yielding ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
cluster non-Empty 1-sorted-yielding TopSpace-yielding ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be TopSpace-yielding ManySortedSet of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> TopStruct ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be TopSpace-yielding ManySortedSet of c₁;
func product_prebasis c₂ -> Subset-Family of (product (Carrier a₂)) means :Def2: :: WAYBEL18:def 2
for b₁ being Subset of (product (Carrier a₂)) holds
( b₁ in a₃ iff ex b₂ being set ex b₃ being TopStruct ex b₄ being Subset of b₃ st
( b₂ in a₁ & b₄ is open & b₃ = a₂ . b₂ & b₁ = product ((Carrier a₂) +* b₂,b₄) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :

theorem Th4: :: WAYBEL18:4

for b₁ being set
for b₂ being Subset-Family of b₁ holds TopStruct(# b₁,(UniCl (FinMeetCl b₂)) #) is TopSpace-like

proof end;

definition

let c₁ be set ;
let c₂ be non-Empty TopSpace-yielding ManySortedSet of c₁;
func product c₂ -> strict TopSpace means :Def3: :: WAYBEL18:def 3
( the carrier of a₃ = product (Carrier a₂) & product_prebasis a₂ is prebasis of a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines product WAYBEL18:def 3 :

registration

let c₁ be set ;
let c₂ be non-Empty TopSpace-yielding ManySortedSet of c₁;
cluster product a₂ -> non empty strict ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non-Empty TopSpace-yielding ManySortedSet of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> non empty TopStruct ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non-Empty TopSpace-yielding ManySortedSet of c₁;
cluster product a₂ -> non empty strict constituted-Functions ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non-Empty TopSpace-yielding ManySortedSet of c₁;
let c₃ be Element of (product c₂);
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of (a₂ . a₄);
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non-Empty TopSpace-yielding ManySortedSet of c₁;
let c₃ be Element of c₁;
func proj c₂,c₃ -> Function of (product a₂),(a₂ . a₃) equals :: WAYBEL18:def 4
proj (Carrier a₂),a₃;
coherence

proof end;

end;

:: deftheorem Def4 defines proj WAYBEL18:def 4 :

theorem Th5: :: WAYBEL18:5

for b₁ being non empty set
for b₂ being non-Empty TopSpace-yielding ManySortedSet of b₁
for b₃ being Element of b₁
for b₄ being Subset of (b₂ . b₃) holds (proj b₂,b₃) " b₄ = product ((Carrier b₂) +* b₃,b₄)

proof end;

theorem Th6: :: WAYBEL18:6

for b₁ being non empty set
for b₂ being non-Empty TopSpace-yielding ManySortedSet of b₁
for b₃ being Element of b₁ holds proj b₂,b₃ is continuous

proof end;

theorem Th7: :: WAYBEL18:7

for b₁ being non empty TopSpace
for b₂ being non empty set
for b₃ being non-Empty TopSpace-yielding ManySortedSet of b₂
for b₄ being Function of b₁,(product b₃) holds
( b₄ is continuous iff for b₅ being Element of b₂ holds (proj b₃,b₅) * b₄ is continuous )

proof end;

definition

let c₁ be TopStruct ;
attr a₁ is injective means :Def5: :: WAYBEL18:def 5
for b₁ being non empty TopSpace
for b₂ being Function of b₁,a₁ st b₂ is continuous holds
for b₃ being non empty TopSpace st b₁ is SubSpace of b₃ holds
ex b₄ being Function of b₃,a₁ st
( b₄ is continuous & b₄ | the carrier of b₁ = b₂ );

end;

:: deftheorem Def5 defines injective WAYBEL18:def 5 :

theorem Th8: :: WAYBEL18:8

for b₁ being non empty set
for b₂ being non-Empty TopSpace-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is injective ) holds
product b₂ is injective

proof end;

theorem Th9: :: WAYBEL18:9

for b₁ being non empty TopSpace st b₁ is injective holds
for b₂ being non empty SubSpace of b₁ st b₂ is_a_retract_of b₁ holds
b₂ is injective

proof end;

definition

let c₁ be 1-sorted ;
let c₂ be TopStruct ;
let c₃ be Function of c₁,c₂;
func Image c₃ -> SubSpace of a₂ equals :: WAYBEL18:def 6
a₂ | (rng a₃);
coherence ;

end;

:: deftheorem Def6 defines Image WAYBEL18:def 6 :

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty TopStruct ;
let c₃ be Function of c₁,c₂;
cluster Image a₃ -> non empty ;
coherence

proof end;

end;

theorem Th10: :: WAYBEL18:10

for b₁ being 1-sorted
for b₂ being TopStruct
for b₃ being Function of b₁,b₂ holds the carrier of (Image b₃) = rng b₃

proof end;

definition

let c₁ be 1-sorted ;
let c₂ be non empty TopStruct ;
let c₃ be Function of c₁,c₂;
func corestr c₃ -> Function of a₁,(Image a₃) equals :: WAYBEL18:def 7
a₃;
coherence

proof end;

end;

:: deftheorem Def7 defines corestr WAYBEL18:def 7 :

theorem Th11: :: WAYBEL18:11

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₃ is continuous holds
corestr b₃ is continuous

proof end;

registration

let c₁ be 1-sorted ;
let c₂ be non empty TopStruct ;
let c₃ be Function of c₁,c₂;
cluster corestr a₃ -> onto ;
coherence

proof end;

end;

definition

let c₁, c₂ be TopStruct ;
pred c₁ is_Retract_of c₂ means :: WAYBEL18:def 8
ex b₁ being Function of a₂,a₂ st
( b₁ is continuous & b₁ * b₁ = b₁ & Image b₁,a₁ are_homeomorphic );

end;

:: deftheorem Def8 defines is_Retract_of WAYBEL18:def 8 :

theorem Th12: :: WAYBEL18:12

for b₁, b₂ being non empty TopSpace st b₁ is injective holds
for b₃ being Function of b₁,b₂ st corestr b₃ is_homeomorphism holds
b₁ is_Retract_of b₂

proof end;

definition

func Sierpinski_Space -> strict TopStruct means :Def9: :: WAYBEL18:def 9
( the carrier of a₁ = {0,1} & the topology of a₁ = {{} ,{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;

Lemma18: Sierpinski_Space is discerning

proof end;

registration

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

end;

registration

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

proof end;

end;

registration

let c₁ be set ;
let c₂ be non empty 1-sorted ;
cluster a₁ --> a₂ -> non-Empty ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be TopStruct ;
cluster a₁ --> a₂ -> 1-sorted-yielding TopSpace-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be reflexive RelStr ;
cluster a₁ --> a₂ -> reflexive-yielding ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty antisymmetric RelStr ;
cluster product (a₁ --> a₂) -> antisymmetric ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty transitive RelStr ;
cluster product (a₁ --> a₂) -> transitive ;
coherence

proof end;

end;

theorem Th13: :: WAYBEL18:13

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

proof end;

theorem Th14: :: WAYBEL18:14

for b₁ being non empty set holds { (product ((Carrier (b₁ --> Sierpinski_Space )) +* b₂,{1})) where B is Element of b₁ : verum } is prebasis of product (b₁ --> Sierpinski_Space )

proof end;

registration

let c₁ be non empty set ;
let c₂ be complete LATTICE;
cluster product (a₁ --> a₂) -> transitive antisymmetric with_suprema complete ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be lower-bounded algebraic LATTICE;
cluster product (a₁ --> a₂) -> transitive antisymmetric algebraic with_suprema complete ;
coherence

proof end;

end;

theorem Th15: :: WAYBEL18:15

for b₁ being non empty set ex b₂ being Function of (BoolePoset b₁),(product (b₁ --> (BoolePoset 1))) st
( b₂ is isomorphic & ( for b₃ being Subset of b₁ holds b₂ . b₃ = chi b₃,b₁ ) )

proof end;

theorem Th16: :: WAYBEL18:16

for b₁ being non empty set
for b₂ being Scott TopAugmentation of product (b₁ --> (BoolePoset 1)) holds the topology of b₂ = the topology of (product (b₁ --> Sierpinski_Space ))

proof end;

theorem Th17: :: WAYBEL18:17

for b₁, b₂ being non empty TopSpace st the carrier of b₁ = the carrier of b₂ & the topology of b₁ = the topology of b₂ & b₁ is injective holds
b₂ is injective

proof end;

theorem Th18: :: WAYBEL18:18

for b₁ being non empty set
for b₂ being Scott TopAugmentation of product (b₁ --> (BoolePoset 1)) holds b₂ is injective

proof end;

theorem Th19: :: WAYBEL18:19

for b₁ being T_0-TopSpace ex b₂ being non empty set ex b₃ being Function of b₁,(product (b₂ --> Sierpinski_Space )) st corestr b₃ is_homeomorphism

proof end;

theorem Th20: :: WAYBEL18:20

for b₁ being T_0-TopSpace st b₁ is injective holds
ex b₂ being non empty set st b₁ is_Retract_of product (b₂ --> Sierpinski_Space )

proof end;