Home | Metamath
Proof Explorer Theorem List (p. 213 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 | discmp 21201 | A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.) |
Theorem | cmpsublem 21202* | Lemma for cmpsub 21203. (Contributed by Jeff Hankins, 28-Jun-2009.) |
↾t ↾t ↾t | ||
Theorem | cmpsub 21203* | Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
↾t | ||
Theorem | tgcmp 21204* | A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 21849, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | cmpcld 21205 | A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.) |
↾t | ||
Theorem | uncmp 21206 | The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.) |
↾t ↾t | ||
Theorem | fiuncmp 21207* | A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.) |
↾t ↾t | ||
Theorem | sscmp 21208 | A subset of a compact topology (i.e. a coarser topology) is compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
TopOn | ||
Theorem | hauscmplem 21209* | Lemma for hauscmp 21210. (Contributed by Mario Carneiro, 27-Nov-2013.) |
↾t | ||
Theorem | hauscmp 21210 | A compact subspace of a T2 space is closed. (Contributed by Jeff Hankins, 16-Jan-2010.) (Proof shortened by Mario Carneiro, 14-Dec-2013.) |
↾t | ||
Theorem | cmpfi 21211* | If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
Theorem | cmpfii 21212 | In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
Theorem | bwth 21213* | The glorious Bolzano-Weierstrass theorem. The first general topology theorem ever proved. The first mention of this theorem can be found in a course by Weierstrass from 1865. In his course Weierstrass called it a lemma. He didn't know how famous this theorem would be. He used a Euclidean space instead of a general compact space. And he was not aware of the Heine-Borel property. But the concepts of neighborhood and limit point were already there although not precisely defined. Cantor was one of his students. He published and used the theorem in an article from 1872. The rest of the general topology followed from that. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) Revised by BL to significantly shorten the proof and avoid infinity, regularity, and choice. (Revised by Brendan Leahy, 26-Dec-2018.) |
Syntax | cconn 21214 | Extend class notation with the class of all connected topologies. |
Conn | ||
Definition | df-conn 21215 | Topologies are connected when only and are both open and closed. (Contributed by FL, 17-Nov-2008.) |
Conn | ||
Theorem | isconn 21216 | The predicate is a connected topology . (Contributed by FL, 17-Nov-2008.) |
Conn | ||
Theorem | isconn2 21217 | The predicate is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.) |
Conn | ||
Theorem | connclo 21218 | The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.) |
Conn | ||
Theorem | conndisj 21219 | If a topology is connected, its underlying set can't be partitioned into two nonempty non-overlapping open sets. (Contributed by FL, 16-Nov-2008.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
Conn | ||
Theorem | conntop 21220 | A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.) |
Conn | ||
Theorem | indisconn 21221 | The indiscrete topology (or trivial topology) on any set is connected. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Conn | ||
Theorem | dfconn2 21222* | An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
TopOn Conn | ||
Theorem | connsuba 21223* | Connectedness for a subspace. See connsub 21224. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
TopOn ↾t Conn | ||
Theorem | connsub 21224* | Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
TopOn ↾t Conn | ||
Theorem | cnconn 21225 | Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
Conn Conn | ||
Theorem | nconnsubb 21226 | Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
TopOn ↾t Conn | ||
Theorem | connsubclo 21227 | If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015.) |
↾t Conn | ||
Theorem | connima 21228 | The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
↾t Conn ↾t Conn | ||
Theorem | conncn 21229 | A continuous function from a connected topology with one point in a clopen set must lie entirely within the set. (Contributed by Mario Carneiro, 16-Feb-2015.) |
Conn | ||
Theorem | iunconnlem 21230* | Lemma for iunconn 21231. (Contributed by Mario Carneiro, 11-Jun-2014.) |
TopOn ↾t Conn | ||
Theorem | iunconn 21231* | The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014.) |
TopOn ↾t Conn ↾t Conn | ||
Theorem | unconn 21232 | The union of two connected overlapping subspaces is connected. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 11-Jun-2014.) |
TopOn ↾t Conn ↾t Conn ↾t Conn | ||
Theorem | clsconn 21233 | The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
TopOn ↾t Conn ↾t Conn | ||
Theorem | conncompid 21234* | The connected component containing contains . (Contributed by Mario Carneiro, 19-Mar-2015.) |
↾t Conn TopOn | ||
Theorem | conncompconn 21235* | The connected component containing is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
↾t Conn TopOn ↾t Conn | ||
Theorem | conncompss 21236* | The connected component containing is a superset of any other connected set containing . (Contributed by Mario Carneiro, 19-Mar-2015.) |
↾t Conn ↾t Conn | ||
Theorem | conncompcld 21237* | The connected component containing is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.) |
↾t Conn TopOn | ||
Theorem | conncompclo 21238* | The connected component containing is a subset of any clopen set containing . (Contributed by Mario Carneiro, 20-Sep-2015.) |
↾t Conn TopOn | ||
Theorem | t1connperf 21239 | A connected T1 space is perfect, unless it is the topology of a singleton. (Contributed by Mario Carneiro, 26-Dec-2016.) |
Conn Perf | ||
Syntax | c1stc 21240 | Extend class definition to include the class of all first-countable topologies. |
Syntax | c2ndc 21241 | Extend class definition to include the class of all second-countable topologies. |
Definition | df-1stc 21242* | Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.) |
Definition | df-2ndc 21243* | Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.) |
Theorem | is1stc 21244* | The predicate "is a first-countable topology." This can be described as "every point has a countable local basis" - that is, every point has a countable collection of open sets containing it such that every open set containing the point has an open set from this collection as a subset. (Contributed by Jeff Hankins, 22-Aug-2009.) |
Theorem | is1stc2 21245* | An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
Theorem | 1stctop 21246 | A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
Theorem | 1stcclb 21247* | A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
Theorem | 1stcfb 21248* | For any point in a first-countable topology, there is a function enumerating neighborhoods of which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015.) |
Theorem | is2ndc 21249* | The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
Theorem | 2ndctop 21250 | A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
Theorem | 2ndci 21251 | A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
Theorem | 2ndcsb 21252* | Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
Theorem | 2ndcredom 21253 | A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.) |
Theorem | 2ndc1stc 21254 | A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) |
Theorem | 1stcrestlem 21255* | Lemma for 1stcrest 21256. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | 1stcrest 21256 | A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
↾t | ||
Theorem | 2ndcrest 21257 | A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
↾t | ||
Theorem | 2ndcctbss 21258* | If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
Theorem | 2ndcdisj 21259* | Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
Theorem | 2ndcdisj2 21260* | Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
Theorem | 2ndcomap 21261* | A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.) |
Theorem | 2ndcsep 21262* | A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015.) |
Theorem | dis2ndc 21263 | A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
Theorem | 1stcelcls 21264* | A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. This proof uses countable choice ax-cc 9257. A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015.) |
Theorem | 1stccnp 21265* | A mapping is continuous at in a first-countable space iff it is sequentially continuous at , meaning that the image under of every sequence converging at converges to . This proof uses ax-cc 9257, but only via 1stcelcls 21264, so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015.) |
TopOn TopOn | ||
Theorem | 1stccn 21266* | A mapping , where is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence converging to , its image under converges to . (Contributed by Mario Carneiro, 7-Sep-2015.) |
TopOn TopOn | ||
Syntax | clly 21267 | Extend class notation with the "locally " predicate of a topological space. |
Locally | ||
Syntax | cnlly 21268 | Extend class notation with the "N-locally " predicate of a topological space. |
𝑛Locally | ||
Definition | df-lly 21269* | Define a space that is locally , where is a topological property like "compact", "connected", or "path-connected". A topological space is locally if every neighborhood of a point contains an open sub-neighborhood that is in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally ↾t | ||
Definition | df-nlly 21270* |
Define a space that is n-locally , where is
a topological
property like "compact", "connected", or
"path-connected". A
topological space is n-locally if every neighborhood of a point
contains a sub-neighborhood that is in the subspace topology.
The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally ". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛Locally in our terminology - open compact sets are not very useful), while others such as "locally connected" are strictly weaker notions if the neighborhoods are not required to be open. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally ↾t | ||
Theorem | islly 21271* | The property of being a locally topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally ↾t | ||
Theorem | isnlly 21272* | The property of being an n-locally topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally ↾t | ||
Theorem | llyeq 21273 | Equality theorem for the Locally predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally Locally | ||
Theorem | nllyeq 21274 | Equality theorem for the Locally predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally 𝑛Locally | ||
Theorem | llytop 21275 | A locally space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally | ||
Theorem | nllytop 21276 | A locally space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally | ||
Theorem | llyi 21277* | The property of a locally topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally ↾t | ||
Theorem | nllyi 21278* | The property of an n-locally topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally ↾t | ||
Theorem | nlly2i 21279* | Eliminate the neighborhood symbol from nllyi 21278. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally ↾t | ||
Theorem | llynlly 21280 | A locally space is n-locally : the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally 𝑛Locally | ||
Theorem | llyssnlly 21281 | A locally space is n-locally . (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally 𝑛Locally | ||
Theorem | llyss 21282 | The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally Locally | ||
Theorem | nllyss 21283 | The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally 𝑛Locally | ||
Theorem | subislly 21284* | The property of a subspace being locally . (Contributed by Mario Carneiro, 10-Mar-2015.) |
↾t Locally ↾t | ||
Theorem | restnlly 21285* | If the property passes to open subspaces, then a space is n-locally iff it is locally . (Contributed by Mario Carneiro, 2-Mar-2015.) |
↾t 𝑛Locally Locally | ||
Theorem | restlly 21286* | If the property passes to open subspaces, then a space which is is also locally . (Contributed by Mario Carneiro, 2-Mar-2015.) |
↾t Locally | ||
Theorem | islly2 21287* | An alternative expression for Locally when passes to open subspaces: A space is locally if every point is contained in an open neighborhood with property . (Contributed by Mario Carneiro, 2-Mar-2015.) |
↾t Locally ↾t | ||
Theorem | llyrest 21288 | An open subspace of a locally space is also locally . (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally ↾t Locally | ||
Theorem | nllyrest 21289 | An open subspace of an n-locally space is also n-locally . (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally ↾t 𝑛Locally | ||
Theorem | loclly 21290 | If is a local property, then both Locally and 𝑛Locally simplify to . (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally 𝑛Locally | ||
Theorem | llyidm 21291 | Idempotence of the "locally" predicate, i.e. being "locally " is a local property. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally Locally Locally | ||
Theorem | nllyidm 21292 | Idempotence of the "n-locally" predicate, i.e. being "n-locally " is a local property. (Use loclly 21290 to show 𝑛Locally 𝑛Locally 𝑛Locally .) (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally 𝑛Locally 𝑛Locally | ||
Theorem | toplly 21293 | A topology is locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally | ||
Theorem | topnlly 21294 | A topology is n-locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally | ||
Theorem | hauslly 21295 | A Hausdorff space is locally Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
Locally | ||
Theorem | hausnlly 21296 | A Hausdorff space is n-locally Hausdorff iff it is locally Hausdorff (both notions are thus referred to as "locally Hausdorff"). (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally Locally | ||
Theorem | hausllycmp 21297 | A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally | ||
Theorem | cldllycmp 21298 | A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 21289.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
𝑛Locally ↾t 𝑛Locally | ||
Theorem | lly1stc 21299 | First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.) |
Locally | ||
Theorem | dislly 21300* | The discrete space is locally if and only if every singleton space has property . (Contributed by Mario Carneiro, 20-Mar-2015.) |
Locally |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |