:: On $T_{1}$ Reflex of Topological Space
:: by Adam Naumowicz and Mariusz {\L}api\'nski
::
:: Received March 7, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PRE_TOPC, EQREL_1, STRUCT_0, SUBSET_1, BORSUK_1,
RELAT_1, TARSKI, CARD_3, RCOMP_1, ZFMISC_1, SETFAM_1, ORDINAL2, FUNCT_1,
T_1TOPSP;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, EQREL_1, TOPS_2,
BORSUK_1;
constructors TOPS_2, BORSUK_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, EQREL_1, STRUCT_0,
PRE_TOPC, BORSUK_1;
requirements BOOLE, SUBSET;
begin
reserve y,w for set;
theorem :: T_1TOPSP:1
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:2
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);
::reserve F for Part-Family of X;
:: Families of partitions of topological spaces
reserve T for non empty TopSpace;
theorem :: T_1TOPSP:3
{ 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 1
{ 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 2
space (Intersection Closed_Partitions T
);
end;
registration
let T;
cluster T_1-reflex T -> strict non empty;
end;
theorem :: T_1TOPSP:4
for T being non empty TopSpace holds T_1-reflex T is T_1;
registration
let T;
cluster T_1-reflex T -> T_1;
end;
registration
cluster T_1 non empty for TopSpace;
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 3
Proj
Intersection Closed_Partitions T;
end;
theorem :: T_1TOPSP:5
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 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:6
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 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:7
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 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:8
for T,T1 being non empty TopSpace,f being continuous Function of
T,T1 holds T1 is T_1 implies ex h being continuous Function 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 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);
end;