:: T_0TOPSP semantic presentation

for A, B being non empty set
for R1, R2 being Relation of A,B st ( for x being Element of A
for y being Element of B holds
( [x,y] in R1 iff [x,y] in R2 ) ) holds
R1 = R2

proof end;

theorem Th2: :: T_0TOPSP:2

for X, Y being non empty set
for f being Function of X,Y
for A being Subset of X st ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds
x2 in A ) holds
f " (f .: A) = A

proof end;

definition

let T, S be TopStruct ;
pred T,S are_homeomorphic means :: T_0TOPSP:def 1
ex f being Function of T,S st f is_homeomorphism ;

end;

:: deftheorem defines are_homeomorphic T_0TOPSP:def 1 :

definition

let T, S be TopStruct ;
let f be Function of T,S;
attr f is open means :Def2: :: T_0TOPSP:def 2
for A being Subset of T st A is open holds
f .: A is open;
correctness ;

end;

:: deftheorem Def2 defines open T_0TOPSP:def 2 :

definition

let T be non empty TopStruct ;
func Indiscernibility T -> Equivalence_Relation of the carrier of T means :Def3: :: T_0TOPSP:def 3
for p, q being Point of T holds
( [p,q] in it iff for A being Subset of T st A is open holds
( p in A iff q in A ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :

definition

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

proof end;

correctness ;

end;

:: deftheorem defines Indiscernible T_0TOPSP:def 4 :

definition

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

end;

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

registration

let T be non empty TopSpace;
cluster T_0-reflex T -> non empty ;
coherence ;

end;

definition

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

end;

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

theorem Th3: :: T_0TOPSP:3

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

theorem Th4: :: T_0TOPSP:4

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

proof end;

theorem Th5: :: T_0TOPSP:5

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

theorem Th6: :: T_0TOPSP:6

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

proof end;

theorem Th7: :: T_0TOPSP:7

for T being non empty TopSpace
for C being set holds
( C is Point of (T_0-reflex T) iff ex p being Point of T st C = Class (Indiscernibility T),p )

proof end;

theorem Th8: :: T_0TOPSP:8

for T being non empty TopSpace
for p being Point of T holds (T_0-canonical_map T) . p = Class (Indiscernibility T),p

proof end;

theorem Th9: :: T_0TOPSP:9

for T being non empty TopSpace
for p, q being Point of T holds
( (T_0-canonical_map T) . q = (T_0-canonical_map T) . p iff [q,p] in Indiscernibility T )

proof end;

theorem Th10: :: T_0TOPSP:10

for T being non empty TopSpace
for A being Subset of T st A is open holds
for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A

proof end;

theorem Th11: :: T_0TOPSP:11

for T being non empty TopSpace
for A being Subset of T st A is open holds
for C being Subset of T st C in Indiscernible T & C meets A holds
C c= A

proof end;

theorem Th12: :: T_0TOPSP:12

for T being non empty TopSpace holds T_0-canonical_map T is open

proof end;

Lm1: for T being non empty TopSpace
for x, y being Point of (T_0-reflex T) st x <> y holds
ex V being Subset of (T_0-reflex T) st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )

proof end;

definition

let IT be TopStruct ;
attr IT is discerning means :Def7: :: T_0TOPSP:def 7
( IT is empty or for x, y being Point of IT st x <> y holds
ex V being Subset of IT st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) );

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

for T being non empty TopSpace holds T_0-reflex T is T_0-TopSpace

proof end;

theorem :: T_0TOPSP:14

for T, S being non empty TopSpace st ex h being Function of (T_0-reflex S),(T_0-reflex T) st
( h is_homeomorphism & T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ) holds
T,S are_homeomorphic

proof end;

theorem Th15: :: T_0TOPSP:15

for T being non empty TopSpace
for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p, q being Point of T st [p,q] in Indiscernibility T holds
f . p = f . q

proof end;

theorem Th16: :: T_0TOPSP:16

for T being non empty TopSpace
for T0 being T_0-TopSpace
for f being continuous Function of T,T0
for p being Point of T holds f .: (Class (Indiscernibility T),p) = {(f . p)}

proof end;

theorem :: T_0TOPSP:17

for T being non empty TopSpace
for T0 being T_0-TopSpace
for f being continuous Function of T,T0 ex h being continuous Function of (T_0-reflex T),T0 st f = h * (T_0-canonical_map T)

proof end;