:: $T_0$ Topological Spaces
:: by Mariusz \.Zynel and Adam Guzowski
::
:: Received May 6, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users


::
:: Preliminaries
::
theorem Th1: :: T_0TOPSP:1
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;

:: Homeomorphic TopSpaces
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 being_homeomorphism ;
end;

:: deftheorem defines are_homeomorphic T_0TOPSP:def 1 :
for T, S being TopStruct holds
( T,S are_homeomorphic iff ex f being Function of T,S st f is being_homeomorphism );

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

:: deftheorem defines open T_0TOPSP:def 2 :
for T, S being TopStruct
for f being Function of T,S holds
( f is open iff for A being Subset of T st A is open holds
f .: A is open );

::
:: Indiscernibility Relation
::
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
ex b1 being Equivalence_Relation of the carrier of T st
for p, q being Point of T holds
( [p,q] in b1 iff for A being Subset of T st A is open holds
( p in A iff q in A ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of the carrier of T st ( for p, q being Point of T holds
( [p,q] in b1 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ) & ( for p, q being Point of T holds
( [p,q] in b2 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :
for T being non empty TopStruct
for b2 being Equivalence_Relation of the carrier of T holds
( b2 = Indiscernibility T iff for p, q being Point of T holds
( [p,q] in b2 iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) );

::
:: Indiscernibility Partition
::
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
Class (Indiscernibility T) is non empty a_partition of the carrier of T
;
end;

:: deftheorem defines Indiscernible T_0TOPSP:def 4 :
for T being non empty TopStruct holds Indiscernible T = Class (Indiscernibility T);

::
:: T_0 Reflex of TopSpace
::
definition
let T be non empty TopSpace;
func T_0-reflex T -> TopSpace equals :: T_0TOPSP:def 5
space (Indiscernible T);
correctness
coherence
space (Indiscernible T) is TopSpace
;
;
end;

:: deftheorem defines T_0-reflex T_0TOPSP:def 5 :
for T being non empty TopSpace holds T_0-reflex T = space (Indiscernible T);

registration
let T be non empty TopSpace;
cluster T_0-reflex T -> non empty ;
coherence
not T_0-reflex T is empty
;
end;

::
:: Function from TopSpace to its T_0 Reflex
::
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
Proj (Indiscernible T) is continuous Function of T,(T_0-reflex T)
;
end;

:: deftheorem defines T_0-canonical_map T_0TOPSP:def 6 :
for T being non empty TopSpace holds T_0-canonical_map T = Proj (Indiscernible T);

theorem Th2: :: T_0TOPSP:2
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 Th3: :: T_0TOPSP:3
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 Th4: :: T_0TOPSP:4
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 Th5: :: T_0TOPSP:5
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 Th6: :: T_0TOPSP:6
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 Th7: :: T_0TOPSP:7
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 Th8: :: T_0TOPSP:8
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;

::
:: Discernible TopStruct
::
definition
let T be TopStruct ;
redefine attr T is T_0 means :Def7: :: T_0TOPSP:def 7
( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) );
compatibility
( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) )
;
end;

:: deftheorem Def7 defines T_0 T_0TOPSP:def 7 :
for T being TopStruct holds
( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) );

registration
cluster non empty TopSpace-like T_0 for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is T_0 & not b1 is empty )
proof end;
end;

::
:: T_0 TopSpace
::
definition
mode T_0-TopSpace is non empty T_0 TopSpace;
end;

theorem :: T_0TOPSP:9
for T being non empty TopSpace holds T_0-reflex T is T_0-TopSpace
proof end;

::
:: Homeomorphism of T_0 Reflexes
::
theorem :: T_0TOPSP:10
for T, S being non empty TopSpace st ex h being Function of (T_0-reflex S),(T_0-reflex T) st
( h is being_homeomorphism & T_0-canonical_map T,h * (T_0-canonical_map S) are_fiberwise_equipotent ) holds
T,S are_homeomorphic
proof end;

::
:: Properties of Continuous Mapping from TopSpace to its T_0 Reflex
::
theorem Th11: :: T_0TOPSP:11
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 Th12: :: T_0TOPSP:12
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;

::
:: Factorization
::
theorem :: T_0TOPSP:13
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;