:: On $T_{1}$ Reflex of Topological Space
:: by Adam Naumowicz and Mariusz {\L}api\'nski
::
:: Received March 7, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users


begin

theorem :: T_1TOPSP:1
canceled;

theorem Th2: :: T_1TOPSP:2
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
proof end;

theorem :: T_1TOPSP:3
canceled;

theorem :: T_1TOPSP:4
canceled;

theorem Th5: :: T_1TOPSP:5
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 )
proof end;

definition
canceled;
canceled;
canceled;
canceled;
end;

:: deftheorem T_1TOPSP:def 1 :
canceled;

:: deftheorem T_1TOPSP:def 2 :
canceled;

:: deftheorem T_1TOPSP:def 3 :
canceled;

:: deftheorem T_1TOPSP:def 4 :
canceled;

theorem :: T_1TOPSP:6
canceled;

theorem :: T_1TOPSP:7
canceled;

theorem :: T_1TOPSP:8
canceled;

theorem :: T_1TOPSP:9
canceled;

theorem :: T_1TOPSP:10
canceled;

theorem Th11: :: T_1TOPSP:11
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;
func Closed_Partitions T -> non empty Part-Family of the carrier of T equals :: T_1TOPSP:def 5
 { 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 } is non empty Part-Family of the carrier of T
proof end;
end;

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

definition
let T be non empty TopSpace;
func T_1-reflex T -> TopSpace equals :: T_1TOPSP:def 6
 space (Intersection (Closed_Partitions T));
correctness
coherence
space (Intersection (Closed_Partitions T)) is TopSpace;
;
end;

:: deftheorem defines T_1-reflex T_1TOPSP:def 6 :
for T being non empty TopSpace holds T_1-reflex T = space (Intersection (Closed_Partitions T));

registration
let T be non empty TopSpace;
cluster T_1-reflex T -> non empty strict ;
coherence
( T_1-reflex T is strict & not T_1-reflex T is empty ) ;
end;

theorem Th12: :: T_1TOPSP:12
for T being non empty TopSpace holds T_1-reflex T is T_1
proof end;

registration
let T be non empty TopSpace;
cluster T_1-reflex T -> T_1 ;
coherence
T_1-reflex T is T_1 by Th12;
end;

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

definition
let T be non empty TopSpace;
func T_1-reflect T -> continuous Function of T,(T_1-reflex T) equals :: T_1TOPSP:def 7
 Proj (Intersection (Closed_Partitions T));
correctness
coherence
Proj (Intersection (Closed_Partitions T)) is continuous Function of T,(T_1-reflex T);
;
end;

:: deftheorem defines T_1-reflect T_1TOPSP:def 7 :
for T being non empty TopSpace holds T_1-reflect T = Proj (Intersection (Closed_Partitions T));

theorem Th13: :: T_1TOPSP:13
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 ) )
proof end;

theorem Th14: :: T_1TOPSP:14
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)}
proof end;

theorem Th15: :: T_1TOPSP:15
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} )
proof end;

theorem Th16: :: T_1TOPSP:16
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)
proof end;

definition
let T, S be non empty TopSpace;
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 8
(T_1-reflect S) * f = it * (T_1-reflect T);
existence
ex b1 being continuous Function of (T_1-reflex T),(T_1-reflex S) st (T_1-reflect S) * f = b1 * (T_1-reflect T) by Th16;
uniqueness
for b1, b2 being continuous Function of (T_1-reflex T),(T_1-reflex S) st (T_1-reflect S) * f = b1 * (T_1-reflect T) & (T_1-reflect S) * f = b2 * (T_1-reflect T) holds
b1 = b2
proof end;
end;

:: deftheorem defines T_1-reflex T_1TOPSP:def 8 :
for T, S being non empty TopSpace
for f being continuous Function of T,S
for b4 being continuous Function of (T_1-reflex T),(T_1-reflex S) holds
( b4 = T_1-reflex f iff (T_1-reflect S) * f = b4 * (T_1-reflect T) );