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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iunconn 22701* | 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 22702 | 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 22703 | The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ (π½ βΎt π΄) β Conn) β (π½ βΎt ((clsβπ½)βπ΄)) β Conn) | ||
Theorem | conncompid 22704* | The connected component containing π΄ contains π΄. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) | ||
Theorem | conncompconn 22705* | The connected component containing π΄ is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π) β Conn) | ||
Theorem | conncompss 22706* | 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 22707* | The connected component containing π΄ is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β (Clsdβπ½)) | ||
Theorem | conncompclo 22708* | 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 22709 | 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 22710 | Extend class definition to include the class of all first-countable topologies. |
class 1stΟ | ||
Syntax | c2ndc 22711 | Extend class definition to include the class of all second-countable topologies. |
class 2ndΟ | ||
Definition | df-1stc 22712* | Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ 1stΟ = {π β Top β£ βπ₯ β βͺ πβπ¦ β π« π(π¦ βΌ Ο β§ βπ§ β π (π₯ β π§ β π₯ β βͺ (π¦ β© π« π§)))} | ||
Definition | df-2ndc 22713* | Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.) |
β’ 2ndΟ = {π β£ βπ₯ β TopBases (π₯ βΌ Ο β§ (topGenβπ₯) = π)} | ||
Theorem | is1stc 22714* | 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 22715* | 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 22716 | A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ (π½ β 1stΟ β π½ β Top) | ||
Theorem | 1stcclb 22717* | A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β 1stΟ β§ π΄ β π) β βπ₯ β π« π½(π₯ βΌ Ο β§ βπ¦ β π½ (π΄ β π¦ β βπ§ β π₯ (π΄ β π§ β§ π§ β π¦)))) | ||
Theorem | 1stcfb 22718* | 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 22719* | 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 22720 | 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 22721 | A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π΅ β TopBases β§ π΅ βΌ Ο) β (topGenβπ΅) β 2ndΟ) | ||
Theorem | 2ndcsb 22722* | 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 22723 | A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ (π½ β 2ndΟ β π½ βΌ β) | ||
Theorem | 2ndc1stc 22724 | A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) |
β’ (π½ β 2ndΟ β π½ β 1stΟ) | ||
Theorem | 1stcrestlem 22725* | Lemma for 1stcrest 22726. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (π΅ βΌ Ο β ran (π₯ β π΅ β¦ πΆ) βΌ Ο) | ||
Theorem | 1stcrest 22726 | A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β 1stΟ β§ π΄ β π) β (π½ βΎt π΄) β 1stΟ) | ||
Theorem | 2ndcrest 22727 | A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β 2ndΟ β§ π΄ β π) β (π½ βΎt π΄) β 2ndΟ) | ||
Theorem | 2ndcctbss 22728* | 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 22729* | 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 22730* | 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 22731* | 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 22732* | 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 22733 | A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ (π βΌ Ο β π« π β 2ndΟ) | ||
Theorem | 1stcelcls 22734* | 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 22735* | 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 22734, 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 22736* | 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 22737 | Extend class notation with the "locally π΄ " predicate of a topological space. |
class Locally π΄ | ||
Syntax | cnlly 22738 | Extend class notation with the "N-locally π΄ " predicate of a topological space. |
class π-Locally π΄ | ||
Definition | df-lly 22739* | 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 22740* |
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 22741* | The property of being a locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β π΄))) | ||
Theorem | isnlly 22742* | The property of being an n-locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) | ||
Theorem | llyeq 22743 | Equality theorem for the Locally π΄ predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ = π΅ β Locally π΄ = Locally π΅) | ||
Theorem | nllyeq 22744 | Equality theorem for the Locally π΄ predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ = π΅ β π-Locally π΄ = π-Locally π΅) | ||
Theorem | llytop 22745 | A locally π΄ space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Locally π΄ β π½ β Top) | ||
Theorem | nllytop 22746 | A locally π΄ space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β π-Locally π΄ β π½ β Top) | ||
Theorem | llyi 22747* | The property of a locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Locally π΄ β§ π β π½ β§ π β π) β βπ’ β π½ (π’ β π β§ π β π’ β§ (π½ βΎt π’) β π΄)) | ||
Theorem | nllyi 22748* | The property of an n-locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄)) | ||
Theorem | nlly2i 22749* | Eliminate the neighborhood symbol from nllyi 22748. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ β π« πβπ’ β π½ (π β π’ β§ π’ β π β§ (π½ βΎt π ) β π΄)) | ||
Theorem | llynlly 22750 | 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 22751 | A locally π΄ space is n-locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally π΄ β π-Locally π΄ | ||
Theorem | llyss 22752 | The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ β π΅ β Locally π΄ β Locally π΅) | ||
Theorem | nllyss 22753 | The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ β π΅ β π-Locally π΄ β π-Locally π΅) | ||
Theorem | subislly 22754* | The property of a subspace being locally π΄. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ ((π½ β Top β§ π΅ β π) β ((π½ βΎt π΅) β Locally π΄ β βπ₯ β π½ βπ¦ β (π₯ β© π΅)βπ’ β π½ ((π’ β© π΅) β π₯ β§ π¦ β π’ β§ (π½ βΎt (π’ β© π΅)) β π΄))) | ||
Theorem | restnlly 22755* | 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 22756* | 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 22757* | 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 22758 | An open subspace of a locally π΄ space is also locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Locally π΄ β§ π΅ β π½) β (π½ βΎt π΅) β Locally π΄) | ||
Theorem | nllyrest 22759 | An open subspace of an n-locally π΄ space is also n-locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π΅ β π½) β (π½ βΎt π΅) β π-Locally π΄) | ||
Theorem | loclly 22760 | If π΄ is a local property, then both Locally π΄ and π-Locally π΄ simplify to π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (Locally π΄ = π΄ β π-Locally π΄ = π΄) | ||
Theorem | llyidm 22761 | 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 22762 | Idempotence of the "n-locally" predicate, i.e. being "n-locally π΄ " is a local property. (Use loclly 22760 to show π-Locally π-Locally π΄ = π-Locally π΄.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally π-Locally π΄ = π-Locally π΄ | ||
Theorem | toplly 22763 | A topology is locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally Top = Top | ||
Theorem | topnlly 22764 | A topology is n-locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π-Locally Top = Top | ||
Theorem | hauslly 22765 | A Hausdorff space is locally Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Haus β π½ β Locally Haus) | ||
Theorem | hausnlly 22766 | 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 22767 | A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Haus β§ π½ β Comp) β π½ β π-Locally Comp) | ||
Theorem | cldllycmp 22768 | A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 22759.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally Comp β§ π΄ β (Clsdβπ½)) β (π½ βΎt π΄) β π-Locally Comp) | ||
Theorem | lly1stc 22769 | First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ Locally 1stΟ = 1stΟ | ||
Theorem | dislly 22770* | The discrete space π« π is locally π΄ if and only if every singleton space has property π΄. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β (π« π β Locally π΄ β βπ₯ β π π« {π₯} β π΄)) | ||
Theorem | disllycmp 22771 | A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β π« π β Locally Comp) | ||
Theorem | dis1stc 22772 | A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π β π β π« π β 1stΟ) | ||
Theorem | hausmapdom 22773 | 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 23261 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 22774 | Simplify the cardinal π΄ββ of hausmapdom 22773 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 22775 | Extend class definition to include the refinement relation. |
class Ref | ||
Syntax | cptfin 22776 | Extend class definition to include the class of point-finite covers. |
class PtFin | ||
Syntax | clocfin 22777 | Extend class definition to include the class of locally finite covers. |
class LocFin | ||
Definition | df-ref 22778* | Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.) |
β’ Ref = {β¨π₯, π¦β© β£ (βͺ π¦ = βͺ π₯ β§ βπ§ β π₯ βπ€ β π¦ π§ β π€)} | ||
Definition | df-ptfin 22779* | Define "point-finite." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ PtFin = {π₯ β£ βπ¦ β βͺ π₯{π§ β π₯ β£ π¦ β π§} β Fin} | ||
Definition | df-locfin 22780* | Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ LocFin = (π₯ β Top β¦ {π¦ β£ (βͺ π₯ = βͺ π¦ β§ βπ β βͺ π₯βπ β π₯ (π β π β§ {π β π¦ β£ (π β© π) β β } β Fin))}) | ||
Theorem | refrel 22781 | Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ Rel Ref | ||
Theorem | isref 22782* | 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 34697. 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 22783 | A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Refπ΅ β π = π) | ||
Theorem | refssex 22784* | 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 22785 | 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 22786 | Reflexivity of refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) |
β’ (π΄ β π β π΄Refπ΄) | ||
Theorem | reftr 22787 | Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ ((π΄Refπ΅ β§ π΅RefπΆ) β π΄RefπΆ) | ||
Theorem | refun0 22788 | Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ ((π΄Refπ΅ β§ π΅ β β ) β (π΄ βͺ {β })Refπ΅) | ||
Theorem | isptfin 22789* | The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π΄ β β’ (π΄ β π΅ β (π΄ β PtFin β βπ₯ β π {π¦ β π΄ β£ π₯ β π¦} β Fin)) | ||
Theorem | islocfin 22790* | The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ (π΄ β (LocFinβπ½) β (π½ β Top β§ π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β } β Fin))) | ||
Theorem | finptfin 22791 | A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ (π΄ β Fin β π΄ β PtFin) | ||
Theorem | ptfinfin 22792* | 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 22793 | A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ ((π½ β Top β§ π΄ β Fin β§ π = π) β π΄ β (LocFinβπ½)) | ||
Theorem | locfintop 22794 | A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ (π΄ β (LocFinβπ½) β π½ β Top) | ||
Theorem | locfinbas 22795 | A locally finite cover must cover the base set of its corresponding topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ (π΄ β (LocFinβπ½) β π = π) | ||
Theorem | locfinnei 22796* | 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 22797 | 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 22798 | Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ ((π΄ β (LocFinβπ½) β§ π΅ β Fin β§ βͺ π΅ β βͺ π½) β (π΄ βͺ π΅) β (LocFinβπ½)) | ||
Theorem | locfincmp 22799 | 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 β§ π = π))) | ||
Theorem | unisngl 22800* | Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π π’ = {π₯}} β β’ π = βͺ πΆ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |