:: T_0TOPSP semantic presentation

theorem Th1: :: T_0TOPSP:1

for b₁, b₂ being non empty set
for b₃, b₄ being Relation of b₁,b₂ st ( for b₅ being Element of b₁
for b₆ being Element of b₂ holds
( [b₅,b₆] in b₃ iff [b₅,b₆] in b₄ ) ) holds
b₃ = b₄

proof end;

theorem Th2: :: T_0TOPSP:2

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ st ( for b₅, b₆ being Element of b₁ st b₅ in b₄ & b₃ . b₅ = b₃ . b₆ holds
b₆ in b₄ ) holds
b₃ " (b₃ .: b₄) = b₄

proof end;

definition

let c₁, c₂ be TopStruct ;
pred c₁,c₂ are_homeomorphic means :: T_0TOPSP:def 1
ex b₁ being Function of a₁,a₂ st b₁ is_homeomorphism ;

end;

:: deftheorem Def1 defines are_homeomorphic T_0TOPSP:def 1 :

definition

let c₁, c₂ be TopStruct ;
let c₃ be Function of c₁,c₂;
attr a₃ is open means :Def2: :: T_0TOPSP:def 2
for b₁ being Subset of a₁ st b₁ is open holds
a₃ .: b₁ is open;
correctness ;

end;

:: deftheorem Def2 defines open T_0TOPSP:def 2 :

definition

let c₁ be non empty TopStruct ;
func Indiscernibility c₁ -> Equivalence_Relation of the carrier of a₁ means :Def3: :: T_0TOPSP:def 3
for b₁, b₂ being Point of a₁ holds
( [b₁,b₂] in a₂ iff for b₃ being Subset of a₁ st b₃ is open holds
( b₁ in b₃ iff b₂ in b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :

definition

let c₁ be non empty TopStruct ;
func Indiscernible c₁ -> non empty a_partition of the carrier of a₁ equals :: T_0TOPSP:def 4
Class (Indiscernibility a₁);
coherence

proof end;

correctness ;

end;

:: deftheorem Def4 defines Indiscernible T_0TOPSP:def 4 :

definition

let c₁ be non empty TopSpace;
func T_0-reflex c₁ -> TopSpace equals :: T_0TOPSP:def 5
space (Indiscernible a₁);
correctness ;

end;

:: deftheorem Def5 defines T_0-reflex T_0TOPSP:def 5 :

registration

let c₁ be non empty TopSpace;
cluster T_0-reflex a₁ -> non empty ;
coherence ;

end;

definition

let c₁ be non empty TopSpace;
func T_0-canonical_map c₁ -> continuous Function of a₁,(T_0-reflex a₁) equals :: T_0TOPSP:def 6
Proj (Indiscernible a₁);
coherence ;

end;

:: deftheorem Def6 defines T_0-canonical_map T_0TOPSP:def 6 :

theorem Th3: :: T_0TOPSP:3

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds b₂ in (T_0-canonical_map b₁) . b₂ by BORSUK_1:70;

theorem Th4: :: T_0TOPSP:4

for b₁ being non empty TopSpace holds
( dom (T_0-canonical_map b₁) = the carrier of b₁ & rng (T_0-canonical_map b₁) c= the carrier of (T_0-reflex b₁) )

proof end;

theorem Th5: :: T_0TOPSP:5

for b₁ being non empty TopSpace holds
( the carrier of (T_0-reflex b₁) = Indiscernible b₁ & the topology of (T_0-reflex b₁) = { b₂ where B is Subset of (Indiscernible b₁) : union b₂ in the topology of b₁ } ) by BORSUK_1:def 10;

theorem Th6: :: T_0TOPSP:6

for b₁ being non empty TopSpace
for b₂ being Subset of (T_0-reflex b₁) holds
( b₂ is open iff union b₂ in the topology of b₁ )

proof end;

theorem Th7: :: T_0TOPSP:7

for b₁ being non empty TopSpace
for b₂ being set holds
( b₂ is Point of (T_0-reflex b₁) iff ex b₃ being Point of b₁ st b₂ = Class (Indiscernibility b₁),b₃ )

proof end;

theorem Th8: :: T_0TOPSP:8

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds (T_0-canonical_map b₁) . b₂ = Class (Indiscernibility b₁),b₂

proof end;

theorem Th9: :: T_0TOPSP:9

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁ holds
( (T_0-canonical_map b₁) . b₃ = (T_0-canonical_map b₁) . b₂ iff [b₃,b₂] in Indiscernibility b₁ )

proof end;

theorem Th10: :: T_0TOPSP:10

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is open holds
for b₃, b₄ being Point of b₁ st b₃ in b₂ & (T_0-canonical_map b₁) . b₃ = (T_0-canonical_map b₁) . b₄ holds
b₄ in b₂

proof end;

theorem Th11: :: T_0TOPSP:11

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is open holds
for b₃ being Subset of b₁ st b₃ in Indiscernible b₁ & b₃ meets b₂ holds
b₃ c= b₂

proof end;

theorem Th12: :: T_0TOPSP:12

for b₁ being non empty TopSpace holds T_0-canonical_map b₁ is open

proof end;

Lemma15: for b₁ being non empty TopSpace
for b₂, b₃ being Point of (T_0-reflex b₁) st b₂ <> b₃ holds
ex b₄ being Subset of (T_0-reflex b₁) st
( b₄ is open & ( ( b₂ in b₄ & not b₃ in b₄ ) or ( b₃ in b₄ & not b₂ in b₄ ) ) )

proof end;

definition

let c₁ be TopStruct ;
attr a₁ is discerning means :Def7: :: T_0TOPSP:def 7
( a₁ is empty or for b₁, b₂ being Point of a₁ st b₁ <> b₂ holds
ex b₃ being Subset of a₁ st
( b₃ is open & ( ( b₁ in b₃ & not b₂ in b₃ ) or ( b₂ in b₃ & not b₁ in b₃ ) ) ) );

end;

:: deftheorem Def7 defines discerning T_0TOPSP:def 7 :

registration

cluster non empty discerning TopStruct ;
existence

proof end;

end;

definition

mode T_0-TopSpace is non empty discerning TopSpace;

end;

theorem Th13: :: T_0TOPSP:13

for b₁ being non empty TopSpace holds T_0-reflex b₁ is T_0-TopSpace

proof end;

theorem Th14: :: T_0TOPSP:14

for b₁, b₂ being non empty TopSpace st ex b₃ being Function of (T_0-reflex b₂),(T_0-reflex b₁) st
( b₃ is_homeomorphism & T_0-canonical_map b₁,b₃ * (T_0-canonical_map b₂) are_fiberwise_equipotent ) holds
b₁,b₂ are_homeomorphic

proof end;

theorem Th15: :: T_0TOPSP:15

for b₁ being non empty TopSpace
for b₂ being T_0-TopSpace
for b₃ being continuous Function of b₁,b₂
for b₄, b₅ being Point of b₁ st [b₄,b₅] in Indiscernibility b₁ holds
b₃ . b₄ = b₃ . b₅

proof end;

theorem Th16: :: T_0TOPSP:16

for b₁ being non empty TopSpace
for b₂ being T_0-TopSpace
for b₃ being continuous Function of b₁,b₂
for b₄ being Point of b₁ holds b₃ .: (Class (Indiscernibility b₁),b₄) = {(b₃ . b₄)}

proof end;

theorem Th17: :: T_0TOPSP:17

for b₁ being non empty TopSpace
for b₂ being T_0-TopSpace
for b₃ being continuous Function of b₁,b₂ ex b₄ being continuous Function of (T_0-reflex b₁),b₂ st b₃ = b₄ * (T_0-canonical_map b₁)

proof end;