:: $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 b₁ being Equivalence_Relation of the carrier of T st
for p, q being Point of T holds
( [p,q] in b₁ iff for A being Subset of T st A is open holds
( p in A iff q in A ) )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of the carrier of T st ( for p, q being Point of T holds
( [p,q] in b₁ 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 b₂ iff for A being Subset of T st A is open holds
( p in A iff q in A ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :
for T being non empty TopStruct
for b₂ being Equivalence_Relation of the carrier of T holds
( b₂ = Indiscernibility T iff for p, q being Point of T holds
( [p,q] in b₂ 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 b₁ being TopSpace st
( b₁ is T_0 & not b₁ 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;