Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### On \Tone\ Reflex of Topological Space

by
Mariusz \Lapinski

MML identifier: T_1TOPSP
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, PRE_TOPC, EQREL_1, BORSUK_1, TARSKI, BOOLE,
SUBSET_1, SETFAM_1, PROB_1, URYSOHN1, ORDINAL2, T_1TOPSP;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
SETFAM_1, STRUCT_0, PRE_TOPC, EQREL_1, TOPS_2, URYSOHN1, BORSUK_1;
constructors URYSOHN1, TOPS_2;
clusters PRE_TOPC, BORSUK_1, STRUCT_0, FSM_1, FUNCT_1, RELSET_1, SUBSET_1,
XBOOLE_0, EQREL_1, PARTFUN1;
requirements BOOLE, SUBSET;

begin

reserve X for non empty set, x for Element of X, y,v,w for set;

canceled;

theorem :: T_1TOPSP:2
for T being non empty TopSpace,
A being non empty a_partition of the carrier of T,
y being Subset of space A holds (Proj(A))"y = union y;

theorem :: T_1TOPSP:3
for X being non empty set,
S being a_partition of X,
A being Subset of S holds (union S) \ (union A) = union (S \ A);

theorem :: T_1TOPSP:4
for X being non empty set,A being Subset of X,
S being a_partition of X holds A in S implies union(S \ {A}) = X \ A;

theorem :: T_1TOPSP:5
for T being non empty TopSpace,
S being non empty a_partition of the carrier of T,
A being Subset of space S,
B being Subset of T holds
B = union A implies (A is closed iff B is closed);

:: Classes of partitions of a set

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

theorem :: T_1TOPSP:6
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;

theorem :: T_1TOPSP:7
for X being non empty set holds {X} is a_partition of X;

definition let X be set;
mode Family-Class of X means
:: T_1TOPSP:def 2
it c= bool bool X;
end;

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

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

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

reserve F for Part-Family of X;

definition
let X be non empty set;
cluster non empty a_partition of X;
end;

theorem :: T_1TOPSP:8
for X being set, p being a_partition of X holds
{p} is Part-Family of X;

definition
let X be set;
cluster non empty Part-Family of X;
end;

theorem :: T_1TOPSP:9
for S1 being a_partition of X,
x,y being Element of X holds
EqClass(x,S1) meets EqClass(y,S1) implies EqClass(x,S1) = EqClass(y,S1);

theorem :: T_1TOPSP:10
for A being set,X being non empty set,S being a_partition of X holds
A in S implies ex x being Element of X st A = EqClass(x,S);

definition
let X be non empty set,F be non empty Part-Family of X;
func Intersection F -> non empty a_partition of X means
:: 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};
end;

:: Families of partitions of topological spaces

reserve T for non empty TopSpace;

theorem :: T_1TOPSP:11
{ A where A is a_partition of the carrier of T : A is closed } is
Part-Family of the carrier of T;

definition
let T;
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 };
end;

:: T_1 reflex of a topological space

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

definition
let T;
cluster T_1-reflex T -> strict non empty;
end;

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

definition let T;
cluster T_1-reflex T -> being_T1;
end;

definition
let T be non empty TopSpace;
func T_1-reflect T -> continuous map of T,T_1-reflex T equals
:: T_1TOPSP:def 7
Proj Intersection Closed_Partitions T;
end;

theorem :: T_1TOPSP:13
for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
T1 is being_T1 implies
({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);

theorem :: T_1TOPSP:14
for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
T1 is being_T1 implies for w for x being Element of T holds
w = EqClass(x,(Intersection Closed_Partitions T)) implies w c= f"{f.x};

theorem :: T_1TOPSP:15
for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
T1 is being_T1 implies
for w st w in the carrier of T_1-reflex T ex z being Element of T1
st z in rng f & w c= f"{z};

:: The theorem on factorization

theorem :: T_1TOPSP:16
for T,T1 being non empty TopSpace,f being continuous map of T,T1 holds
T1 is being_T1 implies
ex h being continuous map of T_1-reflex T, T1 st
f = h*T_1-reflect T;

definition
let T,S be non empty TopSpace;
let f be continuous map of T,S;
func T_1-reflex f -> continuous map of T_1-reflex T, T_1-reflex S means
:: T_1TOPSP:def 8
(T_1-reflect S) * f = it * (T_1-reflect T);
end;
```