:: 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;