Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### \Tzero\ Topological Spaces

**by****Mariusz Zynel, and****Adam Guzowski**- Received May 6, 1994
- MML identifier: T_0TOPSP

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, FUNCT_1, PRE_TOPC, TOPS_2, EQREL_1, RELAT_2, BORSUK_1, SUBSET_1, TARSKI, BOOLE, METRIC_1, RFINSEQ, ORDINAL2, T_0TOPSP, PARTFUN1; notation TARSKI, XBOOLE_0, SUBSET_1, RFINSEQ, RELAT_2, RELSET_1, RELAT_1, FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, PRE_TOPC, TOPS_2, BORSUK_1, EQREL_1; constructors RFINSEQ, RELAT_2, TOPS_2, BORSUK_1, MEMBERED, PARTFUN1, XBOOLE_0; clusters BORSUK_1, RELSET_1, STRUCT_0, PRE_TOPC, SUBSET_1, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_2, XBOOLE_0; requirements SUBSET, BOOLE; begin :: :: Preliminaries :: theorem :: T_0TOPSP:1 for A,B being non empty set, R1,R2 being Relation of A,B st for x being Element of A, y being Element of B holds [x,y] in R1 iff [x,y] in R2 holds R1 = R2; theorem :: T_0TOPSP:2 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 map of T,S st f is_homeomorphism; end; ::::::::::::::::::::::::::::::::::::::::::: :: Open Function :: ::::::::::::::::::::::::::::::::::::::::::: definition let T,S be TopStruct; let f be map 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; definition 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 map of T,T_0-reflex T equals :: T_0TOPSP:def 6 Proj Indiscernible T; end; :: :: Properties of Canonical Map and T_0 Reflex :: theorem :: T_0TOPSP:3 for T being non empty TopSpace, p being Point of T holds p in (T_0-canonical_map(T)).p; theorem :: T_0TOPSP:4 for T being non empty TopSpace holds dom T_0-canonical_map(T) = the carrier of T & rng T_0-canonical_map(T) c= the carrier of T_0-reflex(T); theorem :: T_0TOPSP:5 for T being non empty TopSpace holds the carrier of T_0-reflex(T) = Indiscernible(T) & the topology of T_0-reflex(T) = { A where A is Subset of Indiscernible(T) : union A in the topology of T}; theorem :: T_0TOPSP:6 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:7 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:8 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:9 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:10 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:11 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:12 for T being non empty TopSpace holds T_0-canonical_map(T) is open; :: :: Discernible TopStruct :: definition let IT be TopStruct; attr IT is discerning means :: T_0TOPSP:def 7 IT is empty or for x,y being Point of IT st x <> y holds ex V being Subset of IT st V is open & ((x in V & not y in V) or (y in V & not x in V)); end; definition cluster discerning non empty TopSpace; end; :: :: T_0 TopSpace :: definition mode T_0-TopSpace is discerning non empty TopSpace; end; theorem :: T_0TOPSP:13 for T being non empty TopSpace holds T_0-reflex(T) is T_0-TopSpace; :: :: Homeomorphism of T_0 Reflexes :: theorem :: T_0TOPSP:14 for T,S being non empty TopSpace st ex h being map of T_0-reflex(S),T_0-reflex(T) st h is_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:15 for T being non empty TopSpace, T0 being T_0-TopSpace, f being continuous map 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:16 for T being non empty TopSpace, T0 being T_0-TopSpace, f being continuous map of T,T0 holds for p being Point of T holds f.:Class(Indiscernibility(T),p) = {f.p}; :: :: Factorization :: theorem :: T_0TOPSP:17 for T being non empty TopSpace, T0 being T_0-TopSpace, f being continuous map of T,T0 ex h being continuous map of T_0-reflex(T),T0 st f = h*T_0-canonical_map(T);

Back to top