:: by Adam Naumowicz and Mariusz {\L}api\'nski

::

:: Received March 7, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

theorem Th1: :: T_1TOPSP:1

for T being non empty TopSpace

for A being non empty a_partition of the carrier of T

for y being Subset of (space A) holds (Proj A) " y = union y

for A being non empty a_partition of the carrier of T

for y being Subset of (space A) holds (Proj A) " y = union y

proof end;

theorem Th2: :: T_1TOPSP:2

for T being non empty TopSpace

for S being non empty a_partition of the carrier of T

for A being Subset of (space S)

for B being Subset of T st B = union A holds

( A is closed iff B is closed )

for S being non empty a_partition of the carrier of T

for A being Subset of (space S)

for B being Subset of T st B = union A holds

( A is closed iff B is closed )

proof end;

theorem Th3: :: T_1TOPSP:3

for T being non empty TopSpace holds { A where A is a_partition of the carrier of T : A is closed } is Part-Family of the carrier of T

proof end;

definition

let T be non empty TopSpace;

{ A where A is a_partition of the carrier of T : A is closed } is non empty Part-Family of the carrier of T

end;
func Closed_Partitions T -> non empty Part-Family of the carrier of T equals :: T_1TOPSP:def 1

{ A where A is a_partition of the carrier of T : A is closed } ;

coherence { A where A is a_partition of the carrier of T : A is closed } ;

{ A where A is a_partition of the carrier of T : A is closed } is non empty Part-Family of the carrier of T

proof end;

:: deftheorem defines Closed_Partitions T_1TOPSP:def 1 :

for T being non empty TopSpace holds Closed_Partitions T = { A where A is a_partition of the carrier of T : A is closed } ;

for T being non empty TopSpace holds Closed_Partitions T = { A where A is a_partition of the carrier of T : A is closed } ;

:: T_1 reflex of a topological space

definition

let T be non empty TopSpace;

correctness

coherence

space (Intersection (Closed_Partitions T)) is TopSpace;

;

end;
correctness

coherence

space (Intersection (Closed_Partitions T)) is TopSpace;

;

:: deftheorem defines T_1-reflex T_1TOPSP:def 2 :

for T being non empty TopSpace holds T_1-reflex T = space (Intersection (Closed_Partitions T));

for T being non empty TopSpace holds T_1-reflex T = space (Intersection (Closed_Partitions T));

registration
end;

registration
end;

registration
end;

definition

let T be non empty TopSpace;

coherence

Proj (Intersection (Closed_Partitions T)) is continuous Function of T,(T_1-reflex T);

;

end;
func T_1-reflect T -> continuous Function of T,(T_1-reflex T) equals :: T_1TOPSP:def 3

Proj (Intersection (Closed_Partitions T));

correctness Proj (Intersection (Closed_Partitions T));

coherence

Proj (Intersection (Closed_Partitions T)) is continuous Function of T,(T_1-reflex T);

;

:: deftheorem defines T_1-reflect T_1TOPSP:def 3 :

for T being non empty TopSpace holds T_1-reflect T = Proj (Intersection (Closed_Partitions T));

for T being non empty TopSpace holds T_1-reflect T = Proj (Intersection (Closed_Partitions T));

theorem Th5: :: T_1TOPSP:5

for T, T1 being non empty TopSpace

for f being continuous Function of T,T1 st T1 is T_1 holds

( { (f " {z}) where z is Element of T1 : z in rng f } is a_partition of the carrier of T & ( for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds

A is closed ) )

for f being continuous Function of T,T1 st T1 is T_1 holds

( { (f " {z}) where z is Element of T1 : z in rng f } is a_partition of the carrier of T & ( for A being Subset of T st A in { (f " {z}) where z is Element of T1 : z in rng f } holds

A is closed ) )

proof end;

theorem Th6: :: T_1TOPSP:6

for T, T1 being non empty TopSpace

for f being continuous Function of T,T1 st T1 is T_1 holds

for w being set

for x being Element of T st w = EqClass (x,(Intersection (Closed_Partitions T))) holds

w c= f " {(f . x)}

for f being continuous Function of T,T1 st T1 is T_1 holds

for w being set

for x being Element of T st w = EqClass (x,(Intersection (Closed_Partitions T))) holds

w c= f " {(f . x)}

proof end;

theorem Th7: :: T_1TOPSP:7

for T, T1 being non empty TopSpace

for f being continuous Function of T,T1 st T1 is T_1 holds

for w being set st w in the carrier of (T_1-reflex T) holds

ex z being Element of T1 st

( z in rng f & w c= f " {z} )

for f being continuous Function of T,T1 st T1 is T_1 holds

for w being set st w in the carrier of (T_1-reflex T) holds

ex z being Element of T1 st

( z in rng f & w c= f " {z} )

proof end;

:: The theorem on factorization

theorem Th8: :: T_1TOPSP:8

for T, T1 being non empty TopSpace

for f being continuous Function of T,T1 st T1 is T_1 holds

ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T)

for f being continuous Function of T,T1 st T1 is T_1 holds

ex h being continuous Function of (T_1-reflex T),T1 st f = h * (T_1-reflect T)

proof end;

definition

let T, S be non empty TopSpace;

let f be continuous Function of T,S;

ex b_{1} being continuous Function of (T_1-reflex T),(T_1-reflex S) st (T_1-reflect S) * f = b_{1} * (T_1-reflect T)
by Th8;

uniqueness

for b_{1}, b_{2} being continuous Function of (T_1-reflex T),(T_1-reflex S) st (T_1-reflect S) * f = b_{1} * (T_1-reflect T) & (T_1-reflect S) * f = b_{2} * (T_1-reflect T) holds

b_{1} = b_{2}

end;
let f be continuous Function of T,S;

func T_1-reflex f -> continuous Function of (T_1-reflex T),(T_1-reflex S) means :: T_1TOPSP:def 4

(T_1-reflect S) * f = it * (T_1-reflect T);

existence (T_1-reflect S) * f = it * (T_1-reflect T);

ex b

uniqueness

for b

b

proof end;

:: deftheorem defines T_1-reflex T_1TOPSP:def 4 :

for T, S being non empty TopSpace

for f being continuous Function of T,S

for b_{4} being continuous Function of (T_1-reflex T),(T_1-reflex S) holds

( b_{4} = T_1-reflex f iff (T_1-reflect S) * f = b_{4} * (T_1-reflect T) );

for T, S being non empty TopSpace

for f being continuous Function of T,S

for b

( b