Home | Metamath
Proof Explorer Theorem List (p. 212 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lmcl 21101 | Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
TopOn | ||
Theorem | lmss 21102 | Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
↾t | ||
Theorem | sslm 21103 | A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015.) |
TopOn TopOn | ||
Theorem | lmres 21104 | A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.) |
TopOn | ||
Theorem | lmff 21105* | If converges, there is some upper integer set on which is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
TopOn | ||
Theorem | lmcls 21106* | Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013.) (Revised by Mario Carneiro, 1-May-2014.) |
TopOn | ||
Theorem | lmcld 21107* | Any convergent sequence of points in a closed subset of a topological space converges to a point in the set. (Contributed by Mario Carneiro, 30-Dec-2013.) |
TopOn | ||
Theorem | lmcnp 21108 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) |
Theorem | lmcn 21109 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) |
Syntax | ct0 21110 | Extend class notation with the class of all T0 spaces. |
Syntax | ct1 21111 | Extend class notation to include T1 spaces (also called Fréchet spaces). |
Syntax | cha 21112 | Extend class notation with the class of all Hausdorff spaces. |
Syntax | creg 21113 | Extend class notation with the class of all regular topologies. |
Syntax | cnrm 21114 | Extend class notation with the class of all normal topologies. |
Syntax | ccnrm 21115 | Extend class notation with the class of all completely normal topologies. |
CNrm | ||
Syntax | cpnrm 21116 | Extend class notation with the class of all perfectly normal topologies. |
PNrm | ||
Definition | df-t0 21117* | Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2602): any two points which are members of the same open sets are equal, or in contraposition, for any two distinct points there is an open set which contains one point but not the other. This differs from T1 spaces (see ist1-2 21151) in that in a T1 space you can choose which point will be in the open set and which outside; in a T0 space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Definition | df-t1 21118* | The class of all T1 spaces, also called Fréchet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.) |
Definition | df-haus 21119* | Define the class of all Hausdorff spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98. (Contributed by NM, 8-Mar-2007.) |
Definition | df-reg 21120* | Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Definition | df-nrm 21121* | Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Definition | df-cnrm 21122* | Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
CNrm ↾t | ||
Definition | df-pnrm 21123* | Define perfectly normal spaces. A space is perfectly normal if it is normal and every closed set is a Gδ set, meaning that it is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
PNrm | ||
Theorem | ist0 21124* | The predicate "is a T0 space." Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 21149. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | ist1 21125* | The predicate is T1. (Contributed by FL, 18-Jun-2007.) |
Theorem | ishaus 21126* | Express the predicate " is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
Theorem | iscnrm 21127* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
CNrm ↾t | ||
Theorem | t0sep 21128* | Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | t0dist 21129* | Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | t1sncld 21130 | In a T1 space, one-point sets are closed. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | t1ficld 21131 | In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.) |
Theorem | hausnei 21132* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
Theorem | t0top 21133 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | t1top 21134 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | haustop 21135 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
Theorem | isreg 21136* | The predicate "is a regular space." In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
Theorem | regtop 21137 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | regsep 21138* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | isnrm 21139* | The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.) |
Theorem | nrmtop 21140 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | cnrmtop 21141 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
CNrm | ||
Theorem | iscnrm2 21142* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
TopOn CNrm ↾t | ||
Theorem | ispnrm 21143* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
PNrm | ||
Theorem | pnrmnrm 21144 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
PNrm | ||
Theorem | pnrmtop 21145 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
PNrm | ||
Theorem | pnrmcld 21146* | A closed set in a perfectly normal space is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
PNrm | ||
Theorem | pnrmopn 21147* | An open set in a perfectly normal space is a countable union of closed sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
PNrm | ||
Theorem | ist0-2 21148* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
TopOn | ||
Theorem | ist0-3 21149* | The predicate "is a T0 space," expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
TopOn | ||
Theorem | cnt0 21150 | The preimage of a T0 topology under an injective map is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | ist1-2 21151* | An alternate characterization of T1 spaces. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
TopOn | ||
Theorem | t1t0 21152 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | ist1-3 21153* | A space is T1 iff every point is the only point in the intersection of all open sets containing that point. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
TopOn | ||
Theorem | cnt1 21154 | The preimage of a T1 topology under an injective map is T1. (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | ishaus2 21155* | Express the predicate " is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
TopOn | ||
Theorem | haust1 21156 | A Hausdorff space is a T1 space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
Theorem | hausnei2 21157* | The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009.) |
TopOn | ||
Theorem | cnhaus 21158 | The preimage of a Hausdorff topology under an injective map is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.) |
Theorem | nrmsep3 21159* | In a normal space, given a closed set inside an open set , there is an open set such that . (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | nrmsep2 21160* | In a normal space, any two disjoint closed sets have the property that each one is a subset of an open set whose closure is disjoint from the other. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.) |
Theorem | nrmsep 21161* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | isnrm2 21162* | An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma. (Contributed by Jeff Hankins, 1-Feb-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
Theorem | isnrm3 21163* | A topological space is normal iff any two disjoint closed sets are separated by open sets. (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | cnrmi 21164 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
CNrm ↾t | ||
Theorem | cnrmnrm 21165 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
CNrm | ||
Theorem | restcnrm 21166 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
CNrm ↾t CNrm | ||
Theorem | resthauslem 21167 | Lemma for resthaus 21172 and similar theorems. If the topological property is preserved under injective preimages, then property passes to subspaces. (Contributed by Mario Carneiro, 25-Aug-2015.) |
↾t ↾t ↾t | ||
Theorem | lpcls 21168 | The limit points of the closure of a subset are the same as the limit points of the set in a T1 space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
Theorem | perfcls 21169 | A subset of a perfect space is perfect iff its closure is perfect (and the closure is an actual perfect set, since it is both closed and perfect in the subspace topology). (Contributed by Mario Carneiro, 26-Dec-2016.) |
↾t Perf ↾t Perf | ||
Theorem | restt0 21170 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
↾t | ||
Theorem | restt1 21171 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
↾t | ||
Theorem | resthaus 21172 | A subspace of a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
↾t | ||
Theorem | t1sep2 21173* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | t1sep 21174* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
Theorem | sncld 21175 | A singleton is closed in a Hausdorff space. (Contributed by NM, 5-Mar-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
Theorem | sshauslem 21176 | Lemma for sshaus 21179 and similar theorems. If the topological property is preserved under injective preimages, then a topology finer than one with property also has property . (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | sst0 21177 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | sst1 21178 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | sshaus 21179 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
TopOn | ||
Theorem | regsep2 21180* | In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
Theorem | isreg2 21181* | A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
TopOn | ||
Theorem | dnsconst 21182 | If a continuous mapping to a T1 space is constant on a dense subset, it is constant on the entire space. Note that means " is dense in " and means " is constant on " (see funconstss 6335). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
Theorem | ordtt1 21183 | The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
ordTop | ||
Theorem | lmmo 21184 | A sequence in a Hausdorff space converges to at most one limit. Part of Lemma 1.4-2(a) of [Kreyszig] p. 26. (Contributed by NM, 31-Jan-2008.) (Proof shortened by Mario Carneiro, 1-May-2014.) |
Theorem | lmfun 21185 | The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | dishaus 21186 | A discrete topology is Hausdorff. Morris, Topology without tears, p.72, ex. 13. (Contributed by FL, 24-Jun-2007.) (Proof shortened by Mario Carneiro, 8-Apr-2015.) |
Theorem | ordthauslem 21187* | Lemma for ordthaus 21188. (Contributed by Mario Carneiro, 13-Sep-2015.) |
ordTop ordTop | ||
Theorem | ordthaus 21188 | The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.) |
ordTop | ||
Syntax | ccmp 21189 | Extend class notation with the class of all compact spaces. |
Definition | df-cmp 21190* | Definition of a compact topology. A topology is compact iff any open covering of its underlying set contains a finite sub-covering (Heine-Borel property). Definition C''' of [BourbakiTop1] p. I.59. Note: Bourbaki uses the term quasi-compact topology but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008.) |
Theorem | iscmp 21191* | The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Theorem | cmpcov 21192* | An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.) |
Theorem | cmpcov2 21193* | Rewrite cmpcov 21192 for the cover . (Contributed by Mario Carneiro, 11-Sep-2015.) |
Theorem | cmpcovf 21194* | Combine cmpcov 21192 with ac6sfi 8204 to show the existence of a function that indexes the elements that are generating the open cover. (Contributed by Mario Carneiro, 14-Sep-2014.) |
Theorem | cncmp 21195 | Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
Theorem | fincmp 21196 | A finite topology is compact. (Contributed by FL, 22-Dec-2008.) |
Theorem | 0cmp 21197 | The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.) |
Theorem | cmptop 21198 | A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.) |
Theorem | rncmp 21199 | The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 21-Mar-2015.) |
↾t | ||
Theorem | imacmp 21200 | The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 18-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
↾t ↾t |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |