:: T_1TOPSP semantic presentation

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 Th3: :: T_1TOPSP:3

for X being non empty set
for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)

proof end;

theorem Th4: :: T_1TOPSP:4

for X being non empty set
for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A

proof end;

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

let X be non empty set ;
let x be Element of X;
let S1 be a_partition of X;
func EqClass x,S1 -> Subset of X means :Def1: :: T_1TOPSP:def 1
( x in it & it in S1 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines EqClass T_1TOPSP:def 1 :

theorem Th6: :: T_1TOPSP:6

for X being non empty set
for S1, S2 being a_partition of X st ( for x being Element of X holds EqClass x,S1 = EqClass x,S2 ) holds
S1 = S2

proof end;

theorem Th7: :: T_1TOPSP:7

for X being non empty set holds {X} is a_partition of X

proof end;

definition

let X be set ;
mode Family-Class of X -> set means :Def2: :: T_1TOPSP:def 2
it c= bool (bool X);
existence ;

end;

:: deftheorem Def2 defines Family-Class T_1TOPSP:def 2 :

Lm1: for X being set holds {} is Family-Class of X

proof end;

definition

let X be set ;
let F be Family-Class of X;
attr F is partition-membered means :Def3: :: T_1TOPSP:def 3
for S being set st S in F holds
S is a_partition of X;

end;

:: deftheorem Def3 defines partition-membered T_1TOPSP:def 3 :

registration

let X be set ;
cluster partition-membered Family-Class of X;
existence

proof end;

end;

definition

let X be set ;
mode Part-Family of X is partition-membered Family-Class of X;

end;

registration

let X be non empty set ;
cluster non empty a_partition of X;
existence

proof end;

end;

theorem Th8: :: T_1TOPSP:8

for X being set
for p being a_partition of X holds {p} is Part-Family of X

proof end;

registration

let X be set ;
cluster non empty Family-Class of X;
existence

proof end;

end;

theorem Th9: :: T_1TOPSP:9

for X being non empty set
for S1 being a_partition of X
for x, y being Element of X st EqClass x,S1 meets EqClass y,S1 holds
EqClass x,S1 = EqClass y,S1

proof end;

Lm2: for X being non empty set
for x being Element of X
for F being Part-Family of X
for A being set st A in { (EqClass x,S) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass x,T )

proof end;

theorem Th10: :: T_1TOPSP:10

for A being set
for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass x,S

proof end;

definition

let X be non empty set ;
let F be non empty Part-Family of X;
func Intersection F -> non empty a_partition of X means :Def4: :: T_1TOPSP:def 4
for x being Element of X holds EqClass x,it = meet { (EqClass x,S) where S is a_partition of X : S in F } ;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines Intersection T_1TOPSP:def 4 :

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

proof end;

end;

:: deftheorem defines Closed_Partitions T_1TOPSP:def 5 :

definition

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

end;

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

registration

let T be non empty TopSpace;
cluster T_1-reflex T -> non empty strict ;
coherence ;

end;

theorem Th12: :: T_1TOPSP:12

for T being non empty TopSpace holds T_1-reflex T is being_T1

proof end;

registration

let T be non empty TopSpace;
cluster T_1-reflex T -> non empty strict being_T1 ;
coherence by Th12;

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 ;

end;

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

theorem Th13: :: T_1TOPSP:13

for T, T1 being non empty TopSpace
for f being continuous Function of T,T1 st T1 is being_T1 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 being_T1 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 being_T1 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 being_T1 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 by Th16;
uniqueness

proof end;

end;

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