![]() |
Metamath
Proof Explorer Theorem List (p. 230 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cmpcov2 22901* | Rewrite cmpcov 22900 for the cover {π¦ β π½ β£ π}. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ βπ₯ β π βπ¦ β π½ (π₯ β π¦ β§ π)) β βπ β (π« π½ β© Fin)(π = βͺ π β§ βπ¦ β π π)) | ||
Theorem | cmpcovf 22902* | Combine cmpcov 22900 with ac6sfi 9289 to show the existence of a function that indexes the elements that are generating the open cover. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π½ & β’ (π§ = (πβπ¦) β (π β π)) β β’ ((π½ β Comp β§ βπ₯ β π βπ¦ β π½ (π₯ β π¦ β§ βπ§ β π΄ π)) β βπ β (π« π½ β© Fin)(π = βͺ π β§ βπ(π:π βΆπ΄ β§ βπ¦ β π π))) | ||
Theorem | cncmp 22903 | Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((π½ β Comp β§ πΉ:πβontoβπ β§ πΉ β (π½ Cn πΎ)) β πΎ β Comp) | ||
Theorem | fincmp 22904 | A finite topology is compact. (Contributed by FL, 22-Dec-2008.) |
β’ (π½ β (Top β© Fin) β π½ β Comp) | ||
Theorem | 0cmp 22905 | The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.) |
β’ {β } β Comp | ||
Theorem | cmptop 22906 | A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ (π½ β Comp β π½ β Top) | ||
Theorem | rncmp 22907 | The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β (πΎ βΎt ran πΉ) β Comp) | ||
Theorem | imacmp 22908 | 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.) |
β’ ((πΉ β (π½ Cn πΎ) β§ (π½ βΎt π΄) β Comp) β (πΎ βΎt (πΉ β π΄)) β Comp) | ||
Theorem | discmp 22909 | A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ (π΄ β Fin β π« π΄ β Comp) | ||
Theorem | cmpsublem 22910* | Lemma for cmpsub 22911. (Contributed by Jeff Hankins, 28-Jun-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (βπ β π« π½(π β βͺ π β βπ β (π« π β© Fin)π β βͺ π) β βπ β π« (π½ βΎt π)(βͺ (π½ βΎt π) = βͺ π β βπ‘ β (π« π β© Fin)βͺ (π½ βΎt π) = βͺ π‘))) | ||
Theorem | cmpsub 22911* | 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.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((π½ βΎt π) β Comp β βπ β π« π½(π β βͺ π β βπ β (π« π β© Fin)π β βͺ π))) | ||
Theorem | tgcmp 22912* | A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23556, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π΅ β TopBases β§ π = βͺ π΅) β ((topGenβπ΅) β Comp β βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | cmpcld 22913 | A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ ((π½ β Comp β§ π β (Clsdβπ½)) β (π½ βΎt π) β Comp) | ||
Theorem | uncmp 22914 | The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π = (π βͺ π)) β§ ((π½ βΎt π) β Comp β§ (π½ βΎt π) β Comp)) β π½ β Comp) | ||
Theorem | fiuncmp 22915* | A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ βπ₯ β π΄ (π½ βΎt π΅) β Comp) β (π½ βΎt βͺ π₯ β π΄ π΅) β Comp) | ||
Theorem | sscmp 22916 | A subset of a compact topology (i.e. a coarser topology) is compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π = βͺ πΎ β β’ ((π½ β (TopOnβπ) β§ πΎ β Comp β§ π½ β πΎ) β π½ β Comp) | ||
Theorem | hauscmplem 22917* | Lemma for hauscmp 22918. (Contributed by Mario Carneiro, 27-Nov-2013.) |
β’ π = βͺ π½ & β’ π = {π¦ β π½ β£ βπ€ β π½ (π΄ β π€ β§ ((clsβπ½)βπ€) β (π β π¦))} & β’ (π β π½ β Haus) & β’ (π β π β π) & β’ (π β (π½ βΎt π) β Comp) & β’ (π β π΄ β (π β π)) β β’ (π β βπ§ β π½ (π΄ β π§ β§ ((clsβπ½)βπ§) β (π β π))) | ||
Theorem | hauscmp 22918 | A compact subspace of a T2 space is closed. (Contributed by Jeff Hankins, 16-Jan-2010.) (Proof shortened by Mario Carneiro, 14-Dec-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ π β π β§ (π½ βΎt π) β Comp) β π β (Clsdβπ½)) | ||
Theorem | cmpfi 22919* | 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.) |
β’ (π½ β Top β (π½ β Comp β βπ₯ β π« (Clsdβπ½)(Β¬ β β (fiβπ₯) β β© π₯ β β ))) | ||
Theorem | cmpfii 22920 | 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.) |
β’ ((π½ β Comp β§ π β (Clsdβπ½) β§ Β¬ β β (fiβπ)) β β© π β β ) | ||
Theorem | bwth 22921* | 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.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ π΄ β π β§ Β¬ π΄ β Fin) β βπ₯ β π π₯ β ((limPtβπ½)βπ΄)) | ||
Syntax | cconn 22922 | Extend class notation with the class of all connected topologies. |
class Conn | ||
Definition | df-conn 22923 | Topologies are connected when only β and βͺ π are both open and closed. (Contributed by FL, 17-Nov-2008.) |
β’ Conn = {π β Top β£ (π β© (Clsdβπ)) = {β , βͺ π}} | ||
Theorem | isconn 22924 | The predicate π½ is a connected topology . (Contributed by FL, 17-Nov-2008.) |
β’ π = βͺ π½ β β’ (π½ β Conn β (π½ β Top β§ (π½ β© (Clsdβπ½)) = {β , π})) | ||
Theorem | isconn2 22925 | The predicate π½ is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π = βͺ π½ β β’ (π½ β Conn β (π½ β Top β§ (π½ β© (Clsdβπ½)) β {β , π})) | ||
Theorem | connclo 22926 | The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π = βͺ π½ & β’ (π β π½ β Conn) & β’ (π β π΄ β π½) & β’ (π β π΄ β β ) & β’ (π β π΄ β (Clsdβπ½)) β β’ (π β π΄ = π) | ||
Theorem | conndisj 22927 | 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 22928 | A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.) |
β’ (π½ β Conn β π½ β Top) | ||
Theorem | indisconn 22929 | 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 22930* | An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Conn β βπ₯ β π½ βπ¦ β π½ ((π₯ β β β§ π¦ β β β§ (π₯ β© π¦) = β ) β (π₯ βͺ π¦) β π))) | ||
Theorem | connsuba 22931* | Connectedness for a subspace. See connsub 22932. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((π½ βΎt π΄) β Conn β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β β§ (π¦ β© π΄) β β β§ ((π₯ β© π¦) β© π΄) = β ) β ((π₯ βͺ π¦) β© π΄) β π΄))) | ||
Theorem | connsub 22932* | 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 22933 | Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
β’ π = βͺ πΎ β β’ ((π½ β Conn β§ πΉ:πβontoβπ β§ πΉ β (π½ Cn πΎ)) β πΎ β Conn) | ||
Theorem | nconnsubb 22934 | Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β π) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β (π β© π΄) β β ) & β’ (π β (π β© π΄) β β ) & β’ (π β ((π β© π) β© π΄) = β ) & β’ (π β π΄ β (π βͺ π)) β β’ (π β Β¬ (π½ βΎt π΄) β Conn) | ||
Theorem | connsubclo 22935 | If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π = βͺ π½ & β’ (π β π΄ β π) & β’ (π β (π½ βΎt π΄) β Conn) & β’ (π β π΅ β π½) & β’ (π β (π΅ β© π΄) β β ) & β’ (π β π΅ β (Clsdβπ½)) β β’ (π β π΄ β π΅) | ||
Theorem | connima 22936 | The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π½ & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π΄ β π) & β’ (π β (π½ βΎt π΄) β Conn) β β’ (π β (πΎ βΎt (πΉ β π΄)) β Conn) | ||
Theorem | conncn 22937 | 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) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β πΎ) & β’ (π β π β (ClsdβπΎ)) & β’ (π β π΄ β π) & β’ (π β (πΉβπ΄) β π) β β’ (π β πΉ:πβΆπ) | ||
Theorem | iunconnlem 22938* | Lemma for iunconn 22939. (Contributed by Mario Carneiro, 11-Jun-2014.) |
β’ (π β π½ β (TopOnβπ)) & β’ ((π β§ π β π΄) β π΅ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ ((π β§ π β π΄) β (π½ βΎt π΅) β Conn) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β (π β© βͺ π β π΄ π΅) β β ) & β’ (π β (π β© π) β (π β βͺ π β π΄ π΅)) & β’ (π β βͺ π β π΄ π΅ β (π βͺ π)) & β’ β²ππ β β’ (π β Β¬ π β π) | ||
Theorem | iunconn 22939* | 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 22940 | 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 22941 | The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π β§ (π½ βΎt π΄) β Conn) β (π½ βΎt ((clsβπ½)βπ΄)) β Conn) | ||
Theorem | conncompid 22942* | The connected component containing π΄ contains π΄. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) | ||
Theorem | conncompconn 22943* | The connected component containing π΄ is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π) β Conn) | ||
Theorem | conncompss 22944* | 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 22945* | The connected component containing π΄ is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β (Clsdβπ½)) | ||
Theorem | conncompclo 22946* | 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 22947 | 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 22948 | Extend class definition to include the class of all first-countable topologies. |
class 1stΟ | ||
Syntax | c2ndc 22949 | Extend class definition to include the class of all second-countable topologies. |
class 2ndΟ | ||
Definition | df-1stc 22950* | Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ 1stΟ = {π β Top β£ βπ₯ β βͺ πβπ¦ β π« π(π¦ βΌ Ο β§ βπ§ β π (π₯ β π§ β π₯ β βͺ (π¦ β© π« π§)))} | ||
Definition | df-2ndc 22951* | Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.) |
β’ 2ndΟ = {π β£ βπ₯ β TopBases (π₯ βΌ Ο β§ (topGenβπ₯) = π)} | ||
Theorem | is1stc 22952* | 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 22953* | 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 22954 | A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ (π½ β 1stΟ β π½ β Top) | ||
Theorem | 1stcclb 22955* | A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β 1stΟ β§ π΄ β π) β βπ₯ β π« π½(π₯ βΌ Ο β§ βπ¦ β π½ (π΄ β π¦ β βπ§ β π₯ (π΄ β π§ β§ π§ β π¦)))) | ||
Theorem | 1stcfb 22956* | 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 22957* | 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 22958 | 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 22959 | A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π΅ β TopBases β§ π΅ βΌ Ο) β (topGenβπ΅) β 2ndΟ) | ||
Theorem | 2ndcsb 22960* | 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 22961 | A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ (π½ β 2ndΟ β π½ βΌ β) | ||
Theorem | 2ndc1stc 22962 | A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) |
β’ (π½ β 2ndΟ β π½ β 1stΟ) | ||
Theorem | 1stcrestlem 22963* | Lemma for 1stcrest 22964. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (π΅ βΌ Ο β ran (π₯ β π΅ β¦ πΆ) βΌ Ο) | ||
Theorem | 1stcrest 22964 | A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β 1stΟ β§ π΄ β π) β (π½ βΎt π΄) β 1stΟ) | ||
Theorem | 2ndcrest 22965 | A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β 2ndΟ β§ π΄ β π) β (π½ βΎt π΄) β 2ndΟ) | ||
Theorem | 2ndcctbss 22966* | 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 22967* | 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 22968* | 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 22969* | 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 22970* | 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 22971 | A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ (π βΌ Ο β π« π β 2ndΟ) | ||
Theorem | 1stcelcls 22972* | 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 10432. 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 22973* | 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 10432, but only via 1stcelcls 22972, 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 22974* | 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 22975 | Extend class notation with the "locally π΄ " predicate of a topological space. |
class Locally π΄ | ||
Syntax | cnlly 22976 | Extend class notation with the "N-locally π΄ " predicate of a topological space. |
class π-Locally π΄ | ||
Definition | df-lly 22977* | 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 22978* |
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 22979* | The property of being a locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (π½ β© π« π₯)(π¦ β π’ β§ (π½ βΎt π’) β π΄))) | ||
Theorem | isnlly 22980* | The property of being an n-locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β π-Locally π΄ β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ’ β (((neiβπ½)β{π¦}) β© π« π₯)(π½ βΎt π’) β π΄)) | ||
Theorem | llyeq 22981 | Equality theorem for the Locally π΄ predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ = π΅ β Locally π΄ = Locally π΅) | ||
Theorem | nllyeq 22982 | Equality theorem for the Locally π΄ predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ = π΅ β π-Locally π΄ = π-Locally π΅) | ||
Theorem | llytop 22983 | A locally π΄ space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β Locally π΄ β π½ β Top) | ||
Theorem | nllytop 22984 | A locally π΄ space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π½ β π-Locally π΄ β π½ β Top) | ||
Theorem | llyi 22985* | The property of a locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Locally π΄ β§ π β π½ β§ π β π) β βπ’ β π½ (π’ β π β§ π β π’ β§ (π½ βΎt π’) β π΄)) | ||
Theorem | nllyi 22986* | The property of an n-locally π΄ topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ’ β ((neiβπ½)β{π})(π’ β π β§ (π½ βΎt π’) β π΄)) | ||
Theorem | nlly2i 22987* | Eliminate the neighborhood symbol from nllyi 22986. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π β π½ β§ π β π) β βπ β π« πβπ’ β π½ (π β π’ β§ π’ β π β§ (π½ βΎt π ) β π΄)) | ||
Theorem | llynlly 22988 | 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 22989 | A locally π΄ space is n-locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally π΄ β π-Locally π΄ | ||
Theorem | llyss 22990 | The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ β π΅ β Locally π΄ β Locally π΅) | ||
Theorem | nllyss 22991 | The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (π΄ β π΅ β π-Locally π΄ β π-Locally π΅) | ||
Theorem | subislly 22992* | The property of a subspace being locally π΄. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ ((π½ β Top β§ π΅ β π) β ((π½ βΎt π΅) β Locally π΄ β βπ₯ β π½ βπ¦ β (π₯ β© π΅)βπ’ β π½ ((π’ β© π΅) β π₯ β§ π¦ β π’ β§ (π½ βΎt (π’ β© π΅)) β π΄))) | ||
Theorem | restnlly 22993* | 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 22994* | 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 22995* | 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 22996 | An open subspace of a locally π΄ space is also locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Locally π΄ β§ π΅ β π½) β (π½ βΎt π΅) β Locally π΄) | ||
Theorem | nllyrest 22997 | An open subspace of an n-locally π΄ space is also n-locally π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β π-Locally π΄ β§ π΅ β π½) β (π½ βΎt π΅) β π-Locally π΄) | ||
Theorem | loclly 22998 | If π΄ is a local property, then both Locally π΄ and π-Locally π΄ simplify to π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (Locally π΄ = π΄ β π-Locally π΄ = π΄) | ||
Theorem | llyidm 22999 | 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 23000 | Idempotence of the "n-locally" predicate, i.e. being "n-locally π΄ " is a local property. (Use loclly 22998 to show π-Locally π-Locally π΄ = π-Locally π΄.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ Locally π-Locally π΄ = π-Locally π΄ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |