:: by Mariusz \.Zynel and Adam Guzowski

::

:: Received May 6, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

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

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 ;

end;
pred T,S are_homeomorphic means :: T_0TOPSP:def 1

ex f being Function of T,S st f is being_homeomorphism ;

ex f being Function of T,S st f is being_homeomorphism ;

:: 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 );

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;

;

end;
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 for A being Subset of T st A is open holds

f .: A is open ;

;

:: deftheorem Def2 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 );

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

::

:: Indiscernibility Relation

::

definition

let T be non empty TopStruct ;

ex b_{1} being Equivalence_Relation of the carrier of T st

for p, q being Point of T holds

( [p,q] in b_{1} iff for A being Subset of T st A is open holds

( p in A iff q in A ) )

for b_{1}, b_{2} being Equivalence_Relation of the carrier of T st ( for p, q being Point of T holds

( [p,q] in b_{1} 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_{2} iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for p, q being Point of T holds

( [p,q] in b

( p in A iff q in A ) )

proof end;

uniqueness for b

( [p,q] in b

( p in A iff q in A ) ) ) & ( for p, q being Point of T holds

( [p,q] in b

( p in A iff q in A ) ) ) holds

b

proof end;

:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :

for T being non empty TopStruct

for b_{2} being Equivalence_Relation of the carrier of T holds

( b_{2} = Indiscernibility T iff for p, q being Point of T holds

( [p,q] in b_{2} iff for A being Subset of T st A is open holds

( p in A iff q in A ) ) );

for T being non empty TopStruct

for b

( b

( [p,q] in b

( p in A iff q in A ) ) );

::

:: Indiscernibility Partition

::

:: Indiscernibility Partition

::

definition

let T be non empty TopStruct ;

Class (Indiscernibility T) is non empty a_partition of the carrier of T ;

end;
func Indiscernible T -> non empty a_partition of the carrier of T equals :: T_0TOPSP:def 4

Class (Indiscernibility T);

coherence Class (Indiscernibility T);

Class (Indiscernibility T) is non empty a_partition of the carrier of T ;

:: deftheorem defines Indiscernible T_0TOPSP:def 4 :

for T being non empty TopStruct holds Indiscernible T = Class (Indiscernibility T);

for T being non empty TopStruct holds Indiscernible T = Class (Indiscernibility T);

::

:: T_0 Reflex of TopSpace

::

:: T_0 Reflex of TopSpace

::

definition
end;

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

for T being non empty TopSpace holds T_0-reflex T = space (Indiscernible T);

for T being non empty TopSpace holds T_0-reflex T = space (Indiscernible T);

::

:: Function from TopSpace to its T_0 Reflex

::

:: Function from TopSpace to its T_0 Reflex

::

definition

let T be non empty TopSpace;

Proj (Indiscernible T) is continuous Function of T,(T_0-reflex T) ;

end;
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);

Proj (Indiscernible T) is continuous Function of T,(T_0-reflex T) ;

:: 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);

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 )

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) )

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)

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 )

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

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

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;

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

::

:: Discernible TopStruct

::

definition

let T be TopStruct ;

( 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;
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 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 ) ) ) );

( 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 ) ) ) ) )

proof 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 ) ) ) ) );

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
end;

::

:: T_0 TopSpace

::

:: T_0 TopSpace

::

::

:: Homeomorphism of T_0 Reflexes

::

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

( 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

::

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

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)}

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

::

:: 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)

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;

:: Preliminaries

::