:: T_1TOPSP semantic presentation

theorem Th1: :: T_1TOPSP:1

canceled;

theorem Th2: :: T_1TOPSP:2

for b₁ being non empty TopSpace
for b₂ being non empty a_partition of the carrier of b₁
for b₃ being Subset of (space b₂) holds (Proj b₂) " b₃ = union b₃

proof end;

theorem Th3: :: T_1TOPSP:3

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃ being Subset of b₂ holds (union b₂) \ (union b₃) = union (b₂ \ b₃)

proof end;

theorem Th4: :: T_1TOPSP:4

for b₁ being non empty set
for b₂ being Subset of b₁
for b₃ being a_partition of b₁ st b₂ in b₃ holds
union (b₃ \ {b₂}) = b₁ \ b₂

proof end;

theorem Th5: :: T_1TOPSP:5

for b₁ being non empty TopSpace
for b₂ being non empty a_partition of the carrier of b₁
for b₃ being Subset of (space b₂)
for b₄ being Subset of b₁ st b₄ = union b₃ holds
( b₃ is closed iff b₄ is closed )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be a_partition of c₁;
func EqClass c₂,c₃ -> Subset of a₁ means :Def1: :: T_1TOPSP:def 1
( a₂ in a₄ & a₄ in a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines EqClass T_1TOPSP:def 1 :

theorem Th6: :: T_1TOPSP:6

for b₁ being non empty set
for b₂, b₃ being a_partition of b₁ st ( for b₄ being Element of b₁ holds EqClass b₄,b₂ = EqClass b₄,b₃ ) holds
b₂ = b₃

proof end;

theorem Th7: :: T_1TOPSP:7

for b₁ being non empty set holds {b₁} is a_partition of b₁

proof end;

definition

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

end;

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

Lemma9: for b₁ being set holds {} is Family-Class of b₁

proof end;

definition

let c₁ be set ;
let c₂ be Family-Class of c₁;
attr a₂ is partition-membered means :Def3: :: T_1TOPSP:def 3
for b₁ being set st b₁ in a₂ holds
b₁ is a_partition of a₁;

end;

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

registration

let c₁ be set ;
cluster partition-membered Family-Class of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
mode Part-Family of a₁ is partition-membered Family-Class of a₁;

end;

registration

let c₁ be non empty set ;
cluster non empty a_partition of a₁;
existence

proof end;

end;

theorem Th8: :: T_1TOPSP:8

for b₁ being set
for b₂ being a_partition of b₁ holds {b₂} is Part-Family of b₁

proof end;

registration

let c₁ be set ;
cluster non empty Family-Class of a₁;
existence

proof end;

end;

theorem Th9: :: T_1TOPSP:9

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃, b₄ being Element of b₁ st EqClass b₃,b₂ meets EqClass b₄,b₂ holds
EqClass b₃,b₂ = EqClass b₄,b₂

proof end;

Lemma13: for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Part-Family of b₁
for b₄ being set st b₄ in { (EqClass b₂,b₅) where B is a_partition of b₁ : b₅ in b₃ } holds
ex b₅ being a_partition of b₁ st
( b₅ in b₃ & b₄ = EqClass b₂,b₅ )

proof end;

theorem Th10: :: T_1TOPSP:10

for b₁ being set
for b₂ being non empty set
for b₃ being a_partition of b₂ st b₁ in b₃ holds
ex b₄ being Element of b₂ st b₁ = EqClass b₄,b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Part-Family of c₁;
func Intersection c₂ -> non empty a_partition of a₁ means :Def4: :: T_1TOPSP:def 4
for b₁ being Element of a₁ holds EqClass b₁,a₃ = meet { (EqClass b₁,b₂) where B is a_partition of a₁ : b₂ in a₂ } ;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines Intersection T_1TOPSP:def 4 :

theorem Th11: :: T_1TOPSP:11

for b₁ being non empty TopSpace holds { b₂ where B is a_partition of the carrier of b₁ : b₂ is closed } is Part-Family of the carrier of b₁

proof end;

definition

let c₁ be non empty TopSpace;
func Closed_Partitions c₁ -> non empty Part-Family of the carrier of a₁ equals :: T_1TOPSP:def 5
{ b₁ where B is a_partition of the carrier of a₁ : b₁ is closed } ;
coherence

proof end;

end;

:: deftheorem Def5 defines Closed_Partitions T_1TOPSP:def 5 :

definition

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

end;

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

registration

let c₁ be non empty TopSpace;
cluster T_1-reflex a₁ -> non empty strict ;
coherence ;

end;

theorem Th12: :: T_1TOPSP:12

for b₁ being non empty TopSpace holds T_1-reflex b₁ is being_T1

proof end;

registration

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

end;

definition

let c₁ be non empty TopSpace;
func T_1-reflect c₁ -> continuous Function of a₁,(T_1-reflex a₁) equals :: T_1TOPSP:def 7
Proj (Intersection (Closed_Partitions a₁));
correctness ;

end;

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

theorem Th13: :: T_1TOPSP:13

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₁,b₂ st b₂ is being_T1 holds
( { (b₃ " {b₄}) where B is Element of b₂ : b₄ in rng b₃ } is a_partition of the carrier of b₁ & ( for b₄ being Subset of b₁ st b₄ in { (b₃ " {b₅}) where B is Element of b₂ : b₅ in rng b₃ } holds
b₄ is closed ) )

proof end;

theorem Th14: :: T_1TOPSP:14

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₁,b₂ st b₂ is being_T1 holds
for b₄ being set
for b₅ being Element of b₁ st b₄ = EqClass b₅,(Intersection (Closed_Partitions b₁)) holds
b₄ c= b₃ " {(b₃ . b₅)}

proof end;

theorem Th15: :: T_1TOPSP:15

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₁,b₂ st b₂ is being_T1 holds
for b₄ being set st b₄ in the carrier of (T_1-reflex b₁) holds
ex b₅ being Element of b₂ st
( b₅ in rng b₃ & b₄ c= b₃ " {b₅} )

proof end;

theorem Th16: :: T_1TOPSP:16

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₁,b₂ st b₂ is being_T1 holds
ex b₄ being continuous Function of (T_1-reflex b₁),b₂ st b₃ = b₄ * (T_1-reflect b₁)

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be continuous Function of c₁,c₂;
func T_1-reflex c₃ -> continuous Function of (T_1-reflex a₁),(T_1-reflex a₂) means :: T_1TOPSP:def 8
(T_1-reflect a₂) * a₃ = a₄ * (T_1-reflect a₁);
existence by Th16;
uniqueness

proof end;

end;

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