Home | Metamath
Proof Explorer Theorem List (p. 228 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iunconnlem 22701* | Lemma for iunconn 22702. (Contributed by Mario Carneiro, 11-Jun-2014.) |
β’ (π β π½ β (TopOnβπ)) & β’ ((π β§ π β π΄) β π΅ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ ((π β§ π β π΄) β (π½ βΎt π΅) β Conn) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β (π β© βͺ π β π΄ π΅) β β ) & β’ (π β (π β© π) β (π β βͺ π β π΄ π΅)) & β’ (π β βͺ π β π΄ π΅ β (π βͺ π)) & β’ β²ππ β β’ (π β Β¬ π β π) | ||
Theorem | iunconn 22702* | 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 22703 | 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 22704 | The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ (π½ βΎt π΄) β Conn) β (π½ βΎt ((clsβπ½)βπ΄)) β Conn) | ||
Theorem | conncompid 22705* | The connected component containing π΄ contains π΄. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) | ||
Theorem | conncompconn 22706* | The connected component containing π΄ is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π) β Conn) | ||
Theorem | conncompss 22707* | 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 22708* | The connected component containing π΄ is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β (Clsdβπ½)) | ||
Theorem | conncompclo 22709* | The connected component containing π΄ is a subset of any clopen set containing π΄. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π β (π½ β© (Clsdβπ½)) β§ π΄ β π) β π β π) | ||
Theorem | t1connperf 22710 | A connected T1 space is perfect, unless it is the topology of a singleton. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π½ β Conn β§ Β¬ π β 1o) β π½ β Perf) | ||
Syntax | c1stc 22711 | Extend class definition to include the class of all first-countable topologies. |
class 1stΟ | ||
Syntax | c2ndc 22712 | Extend class definition to include the class of all second-countable topologies. |
class 2ndΟ | ||
Definition | df-1stc 22713* | Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ 1stΟ = {π β Top β£ βπ₯ β βͺ πβπ¦ β π« π(π¦ βΌ Ο β§ βπ§ β π (π₯ β π§ β π₯ β βͺ (π¦ β© π« π§)))} | ||
Definition | df-2ndc 22714* | Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.) |
β’ 2ndΟ = {π β£ βπ₯ β TopBases (π₯ βΌ Ο β§ (topGenβπ₯) = π)} | ||
Theorem | is1stc 22715* | 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.) |
β’ π = βͺ π½ β β’ (π½ β 1stΟ β (π½ β Top β§ βπ₯ β π βπ¦ β π« π½(π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β π₯ β βͺ (π¦ β© π« π§))))) | ||
Theorem | is1stc2 22716* | An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
β’ π = βͺ π½ β β’ (π½ β 1stΟ β (π½ β Top β§ βπ₯ β π βπ¦ β π« π½(π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§))))) | ||
Theorem | 1stctop 22717 | A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ (π½ β 1stΟ β π½ β Top) | ||
Theorem | 1stcclb 22718* | A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β 1stΟ β§ π΄ β π) β βπ₯ β π« π½(π₯ βΌ Ο β§ βπ¦ β π½ (π΄ β π¦ β βπ§ β π₯ (π΄ β π§ β§ π§ β π¦)))) | ||
Theorem | 1stcfb 22719* | 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.) |
β’ π = βͺ π½ β β’ ((π½ β 1stΟ β§ π΄ β π) β βπ(π:ββΆπ½ β§ βπ β β (π΄ β (πβπ) β§ (πβ(π + 1)) β (πβπ)) β§ βπ¦ β π½ (π΄ β π¦ β βπ β β (πβπ) β π¦))) | ||
Theorem | is2ndc 22720* | The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
β’ (π½ β 2ndΟ β βπ₯ β TopBases (π₯ βΌ Ο β§ (topGenβπ₯) = π½)) | ||
Theorem | 2ndctop 22721 | A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
β’ (π½ β 2ndΟ β π½ β Top) | ||
Theorem | 2ndci 22722 | A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π΅ β TopBases β§ π΅ βΌ Ο) β (topGenβπ΅) β 2ndΟ) | ||
Theorem | 2ndcsb 22723* | 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.) |
β’ (π½ β 2ndΟ β βπ₯(π₯ βΌ Ο β§ (topGenβ(fiβπ₯)) = π½)) | ||
Theorem | 2ndcredom 22724 | A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ (π½ β 2ndΟ β π½ βΌ β) | ||
Theorem | 2ndc1stc 22725 | A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) |
β’ (π½ β 2ndΟ β π½ β 1stΟ) | ||
Theorem | 1stcrestlem 22726* | Lemma for 1stcrest 22727. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (π΅ βΌ Ο β ran (π₯ β π΅ β¦ πΆ) βΌ Ο) | ||
Theorem | 1stcrest 22727 | A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β 1stΟ β§ π΄ β π) β (π½ βΎt π΄) β 1stΟ) | ||
Theorem | 2ndcrest 22728 | A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β 2ndΟ β§ π΄ β π) β (π½ βΎt π΄) β 2ndΟ) | ||
Theorem | 2ndcctbss 22729* | 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.) |
β’ π½ = (topGenβπ΅) & β’ π = {β¨π’, π£β© β£ (π’ β π β§ π£ β π β§ βπ€ β π΅ (π’ β π€ β§ π€ β π£))} β β’ ((π΅ β TopBases β§ π½ β 2ndΟ) β βπ β TopBases (π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ))) | ||
Theorem | 2ndcdisj 22730* | 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.) |
β’ ((π½ β 2ndΟ β§ βπ₯ β π΄ π΅ β (π½ β {β }) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο) | ||
Theorem | 2ndcdisj2 22731* | 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.) |
β’ ((π½ β 2ndΟ β§ π΄ β π½ β§ βπ¦β*π₯ β π΄ π¦ β π₯) β π΄ βΌ Ο) | ||
Theorem | 2ndcomap 22732* | A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ πΎ & β’ (π β π½ β 2ndΟ) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β ran πΉ = π) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΎ) β β’ (π β πΎ β 2ndΟ) | ||
Theorem | 2ndcsep 22733* | A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ π = βͺ π½ β β’ (π½ β 2ndΟ β βπ₯ β π« π(π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π)) | ||
Theorem | dis2ndc 22734 | A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ (π βΌ Ο β π« π β 2ndΟ) | ||
Theorem | 1stcelcls 22735* | 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 10305. 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.) |
β’ π = βͺ π½ β β’ ((π½ β 1stΟ β§ π β π) β (π β ((clsβπ½)βπ) β βπ(π:ββΆπ β§ π(βπ‘βπ½)π))) | ||
Theorem | 1stccnp 22736* | 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 10305, but only via 1stcelcls 22735, 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.) |
β’ (π β π½ β 1stΟ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ))))) | ||
Theorem | 1stccn 22737* | 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.) |
β’ (π β π½ β 1stΟ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ β (π½ Cn πΎ) β βπ(π:ββΆπ β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) | ||
Syntax | clly 22738 | Extend class notation with the "locally π΄ " predicate of a topological space. |
class Locally π΄ | ||
Syntax | cnlly 22739 | Extend class notation with the "N-locally π΄ " predicate of a topological space. |
class π-Locally π΄ | ||
Definition | df-lly 22740* | 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 subneighborhood that is π΄ in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally π΄ = {π β Top β£ βπ₯ β π βπ¦ β π₯ βπ’ β (π β© π« π₯)(π¦ β π’ β§ (π βΎt π’) β π΄)} | ||
Definition | df-nlly 22741* |
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 subneighborhood 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 Comp 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 π΄ = {π β Top β£ βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄} | ||
Theorem | islly 22742* | The property of being a locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β π΄))) | ||
Theorem | isnlly 22743* | The property of being an n-locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) | ||
Theorem | llyeq 22744 | Equality theorem for the Locally π΄ predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ = π΅ β Locally π΄ = Locally π΅) | ||
Theorem | nllyeq 22745 | Equality theorem for the Locally π΄ predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ = π΅ β π-Locally π΄ = π-Locally π΅) | ||
Theorem | llytop 22746 | A locally π΄ space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Locally π΄ β π½ β Top) | ||
Theorem | nllytop 22747 | A locally π΄ space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β π-Locally π΄ β π½ β Top) | ||
Theorem | llyi 22748* | The property of a locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Locally π΄ β§ π β π½ β§ π β π) β βπ’ β π½ (π’ β π β§ π β π’ β§ (π½ βΎt π’) β π΄)) | ||
Theorem | nllyi 22749* | The property of an n-locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄)) | ||
Theorem | nlly2i 22750* | Eliminate the neighborhood symbol from nllyi 22749. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ β π« πβπ’ β π½ (π β π’ β§ π’ β π β§ (π½ βΎt π ) β π΄)) | ||
Theorem | llynlly 22751 | 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 22752 | A locally π΄ space is n-locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally π΄ β π-Locally π΄ | ||
Theorem | llyss 22753 | The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ β π΅ β Locally π΄ β Locally π΅) | ||
Theorem | nllyss 22754 | The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ β π΅ β π-Locally π΄ β π-Locally π΅) | ||
Theorem | subislly 22755* | The property of a subspace being locally π΄. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ ((π½ β Top β§ π΅ β π) β ((π½ βΎt π΅) β Locally π΄ β βπ₯ β π½ βπ¦ β (π₯ β© π΅)βπ’ β π½ ((π’ β© π΅) β π₯ β§ π¦ β π’ β§ (π½ βΎt (π’ β© π΅)) β π΄))) | ||
Theorem | restnlly 22756* | 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 22757* | If the property π΄ passes to open subspaces, then a space which is π΄ is also locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π β§ (π β π΄ β§ π₯ β π)) β (π βΎt π₯) β π΄) & β’ (π β π΄ β Top) β β’ (π β π΄ β Locally π΄) | ||
Theorem | islly2 22758* | 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 π΄ β (π½ β Top β§ βπ¦ β π βπ’ β π½ (π¦ β π’ β§ (π½ βΎt π’) β π΄)))) | ||
Theorem | llyrest 22759 | An open subspace of a locally π΄ space is also locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Locally π΄ β§ π΅ β π½) β (π½ βΎt π΅) β Locally π΄) | ||
Theorem | nllyrest 22760 | An open subspace of an n-locally π΄ space is also n-locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π΅ β π½) β (π½ βΎt π΅) β π-Locally π΄) | ||
Theorem | loclly 22761 | If π΄ is a local property, then both Locally π΄ and π-Locally π΄ simplify to π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (Locally π΄ = π΄ β π-Locally π΄ = π΄) | ||
Theorem | llyidm 22762 | 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 22763 | Idempotence of the "n-locally" predicate, i.e. being "n-locally π΄ " is a local property. (Use loclly 22761 to show π-Locally π-Locally π΄ = π-Locally π΄.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally π-Locally π΄ = π-Locally π΄ | ||
Theorem | toplly 22764 | A topology is locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally Top = Top | ||
Theorem | topnlly 22765 | A topology is n-locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π-Locally Top = Top | ||
Theorem | hauslly 22766 | A Hausdorff space is locally Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Haus β π½ β Locally Haus) | ||
Theorem | hausnlly 22767 | 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 Haus β π½ β Locally Haus) | ||
Theorem | hausllycmp 22768 | A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Haus β§ π½ β Comp) β π½ β π-Locally Comp) | ||
Theorem | cldllycmp 22769 | A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 22760.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally Comp β§ π΄ β (Clsdβπ½)) β (π½ βΎt π΄) β π-Locally Comp) | ||
Theorem | lly1stc 22770 | First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ Locally 1stΟ = 1stΟ | ||
Theorem | dislly 22771* | The discrete space π« π is locally π΄ if and only if every singleton space has property π΄. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β (π« π β Locally π΄ β βπ₯ β π π« {π₯} β π΄)) | ||
Theorem | disllycmp 22772 | A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β π« π β Locally Comp) | ||
Theorem | dis1stc 22773 | A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π β π β π« π β 1stΟ) | ||
Theorem | hausmapdom 22774 | If π is a first-countable Hausdorff space, then the cardinality of the closure of a set π΄ is bounded by β to the power π΄. In particular, a first-countable Hausdorff space with a dense subset π΄ has cardinality at most π΄ββ, and a separable first-countable Hausdorff space has cardinality at most π« β. (Compare hauspwpwdom 23262 to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ π½ β 1stΟ β§ π΄ β π) β ((clsβπ½)βπ΄) βΌ (π΄ βm β)) | ||
Theorem | hauspwdom 22775 | Simplify the cardinal π΄ββ of hausmapdom 22774 to π« π΅ = 2βπ΅ when π΅ is an infinite cardinal greater than π΄. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π = βͺ π½ β β’ (((π½ β Haus β§ π½ β 1stΟ β§ π΄ β π) β§ (π΄ βΌ π« π΅ β§ β βΌ π΅)) β ((clsβπ½)βπ΄) βΌ π« π΅) | ||
Syntax | cref 22776 | Extend class definition to include the refinement relation. |
class Ref | ||
Syntax | cptfin 22777 | Extend class definition to include the class of point-finite covers. |
class PtFin | ||
Syntax | clocfin 22778 | Extend class definition to include the class of locally finite covers. |
class LocFin | ||
Definition | df-ref 22779* | Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.) |
β’ Ref = {β¨π₯, π¦β© β£ (βͺ π¦ = βͺ π₯ β§ βπ§ β π₯ βπ€ β π¦ π§ β π€)} | ||
Definition | df-ptfin 22780* | Define "point-finite." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ PtFin = {π₯ β£ βπ¦ β βͺ π₯{π§ β π₯ β£ π¦ β π§} β Fin} | ||
Definition | df-locfin 22781* | Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ LocFin = (π₯ β Top β¦ {π¦ β£ (βͺ π₯ = βͺ π¦ β§ βπ β βͺ π₯βπ β π₯ (π β π β§ {π β π¦ β£ (π β© π) β β } β Fin))}) | ||
Theorem | refrel 22782 | Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ Rel Ref | ||
Theorem | isref 22783* | The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne 34707. On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄ β πΆ β (π΄Refπ΅ β (π = π β§ βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦))) | ||
Theorem | refbas 22784 | A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Refπ΅ β π = π) | ||
Theorem | refssex 22785* | Every set in a refinement has a superset in the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ ((π΄Refπ΅ β§ π β π΄) β βπ₯ β π΅ π β π₯) | ||
Theorem | ssref 22786 | A subcover is a refinement of the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ ((π΄ β πΆ β§ π΄ β π΅ β§ π = π) β π΄Refπ΅) | ||
Theorem | refref 22787 | Reflexivity of refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) |
β’ (π΄ β π β π΄Refπ΄) | ||
Theorem | reftr 22788 | Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ ((π΄Refπ΅ β§ π΅RefπΆ) β π΄RefπΆ) | ||
Theorem | refun0 22789 | Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ ((π΄Refπ΅ β§ π΅ β β ) β (π΄ βͺ {β })Refπ΅) | ||
Theorem | isptfin 22790* | The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π΄ β β’ (π΄ β π΅ β (π΄ β PtFin β βπ₯ β π {π¦ β π΄ β£ π₯ β π¦} β Fin)) | ||
Theorem | islocfin 22791* | The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ (π΄ β (LocFinβπ½) β (π½ β Top β§ π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β } β Fin))) | ||
Theorem | finptfin 22792 | A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ (π΄ β Fin β π΄ β PtFin) | ||
Theorem | ptfinfin 22793* | A point covered by a point-finite cover is only covered by finitely many elements. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π΄ β β’ ((π΄ β PtFin β§ π β π) β {π₯ β π΄ β£ π β π₯} β Fin) | ||
Theorem | finlocfin 22794 | A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ ((π½ β Top β§ π΄ β Fin β§ π = π) β π΄ β (LocFinβπ½)) | ||
Theorem | locfintop 22795 | A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ (π΄ β (LocFinβπ½) β π½ β Top) | ||
Theorem | locfinbas 22796 | A locally finite cover must cover the base set of its corresponding topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ (π΄ β (LocFinβπ½) β π = π) | ||
Theorem | locfinnei 22797* | A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ β β’ ((π΄ β (LocFinβπ½) β§ π β π) β βπ β π½ (π β π β§ {π β π΄ β£ (π β© π) β β } β Fin)) | ||
Theorem | lfinpfin 22798 | A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π΄ β (LocFinβπ½) β π΄ β PtFin) | ||
Theorem | lfinun 22799 | Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ ((π΄ β (LocFinβπ½) β§ π΅ β Fin β§ βͺ π΅ β βͺ π½) β (π΄ βͺ π΅) β (LocFinβπ½)) | ||
Theorem | locfincmp 22800 | For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΆ β β’ (π½ β Comp β (πΆ β (LocFinβπ½) β (πΆ β Fin β§ π = π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |