:: $T_0$ Topological Spaces :: by Mariusz \.Zynel and Adam Guzowski :: :: Received May 6, 1994 :: Copyright (c) 1994-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, FUNCT_1, SUBSET_1, RELAT_1, TARSKI, PRE_TOPC, TOPS_2, RCOMP_1, EQREL_1, STRUCT_0, RELAT_2, BORSUK_1, ORDINAL2, CARD_3, CLASSES1, T_0TOPSP, FUNCT_2; notations TARSKI, XBOOLE_0, SUBSET_1, CLASSES1, RELAT_2, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_2, BORSUK_1, EQREL_1; constructors SETFAM_1, RFINSEQ, TOPS_2, BORSUK_1, CLASSES1; registrations XBOOLE_0, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC, BORSUK_1, EQREL_1, RELSET_1; requirements SUBSET, BOOLE; begin :: :: Preliminaries :: theorem :: T_0TOPSP:1 for X,Y being non empty set, f being Function of X,Y holds for A being Subset of X st for x1,x2 being Element of X holds x1 in A & f.x1=f.x2 implies x2 in A holds f"(f.:A) = A; :: Homeomorphic TopSpaces definition let T,S be TopStruct; pred T,S are_homeomorphic means :: T_0TOPSP:def 1 ex f being Function of T,S st f is being_homeomorphism; end; :: Open Function definition let T,S be TopStruct; let f be Function of T,S; attr f is open means :: T_0TOPSP:def 2 for A being Subset of T st A is open holds f.:A is open; end; :: :: Indiscernibility Relation :: definition let T be non empty TopStruct; func Indiscernibility(T) -> Equivalence_Relation of the carrier of T means :: T_0TOPSP:def 3 for p,q being Point of T holds [p,q] in it iff for A being Subset of T st A is open holds p in A iff q in A; end; :: :: Indiscernibility Partition :: definition let T be non empty TopStruct; func Indiscernible(T) -> non empty a_partition of the carrier of T equals :: T_0TOPSP:def 4 Class Indiscernibility(T); end; :: :: T_0 Reflex of TopSpace :: definition let T be non empty TopSpace; func T_0-reflex(T) -> TopSpace equals :: T_0TOPSP:def 5 space Indiscernible(T); end; registration let T be non empty TopSpace; cluster T_0-reflex(T) -> non empty; end; :: :: Function from TopSpace to its T_0 Reflex :: definition let T be non empty TopSpace; func T_0-canonical_map T -> continuous Function of T,T_0-reflex T equals :: T_0TOPSP:def 6 Proj Indiscernible T; end; theorem :: T_0TOPSP:2 for T being non empty TopSpace, V being Subset of T_0-reflex(T) holds V is open iff union V in the topology of T; theorem :: T_0TOPSP:3 for T being non empty TopSpace, C being set holds C is Point of T_0-reflex(T) iff ex p being Point of T st C = Class(Indiscernibility(T),p); theorem :: T_0TOPSP:4 for T being non empty TopSpace, p being Point of T holds ( T_0-canonical_map(T)).p = Class(Indiscernibility(T),p); theorem :: T_0TOPSP:5 for T being non empty TopSpace, p,q being Point of T holds ( T_0-canonical_map(T)).q = (T_0-canonical_map(T)).p iff [q,p] in Indiscernibility(T); theorem :: T_0TOPSP:6 for T being non empty TopSpace, A being Subset of T st A is open holds for p,q being Point of T holds p in A & (T_0-canonical_map(T)).p = ( T_0-canonical_map(T)).q implies q in A; theorem :: T_0TOPSP:7 for T being non empty TopSpace, A being Subset of T st A is open for C being Subset of T st C in Indiscernible(T) & C meets A holds C c= A; theorem :: T_0TOPSP:8 for T being non empty TopSpace holds T_0-canonical_map(T) is open; :: :: Discernible TopStruct :: definition let T be TopStruct; redefine attr T is T_0 means :: T_0TOPSP:def 7 T is empty or for x,y being Point of T st x <> y holds ex V being Subset of T st V is open & ( x in V & not y in V or y in V & not x in V ); end; registration cluster T_0 non empty for TopSpace; end; :: :: T_0 TopSpace :: definition mode T_0-TopSpace is T_0 non empty TopSpace; end; theorem :: T_0TOPSP:9 for T being non empty TopSpace holds T_0-reflex(T) is T_0-TopSpace; :: :: Homeomorphism of T_0 Reflexes :: theorem :: T_0TOPSP:10 for T,S being non empty TopSpace st ex h being Function of T_0-reflex( S),T_0-reflex(T) st h is being_homeomorphism & T_0-canonical_map(T),h* T_0-canonical_map(S) are_fiberwise_equipotent holds T,S are_homeomorphic; :: :: Properties of Continuous Mapping from TopSpace to its T_0 Reflex :: theorem :: T_0TOPSP:11 for T being non empty TopSpace, T0 being T_0-TopSpace, f being continuous Function of T,T0 holds for p,q being Point of T holds [p,q] in Indiscernibility(T) implies f.p = f.q; theorem :: T_0TOPSP:12 for T being non empty TopSpace, T0 being T_0-TopSpace, f being continuous Function of T,T0 holds for p being Point of T holds f.:Class( Indiscernibility(T),p) = {f.p}; :: :: Factorization :: theorem :: T_0TOPSP:13 for T being non empty TopSpace, T0 being T_0-TopSpace, f being continuous Function of T,T0 ex h being continuous Function of T_0-reflex(T),T0 st f = h*T_0-canonical_map(T);