![]() |
Metamath
Proof Explorer Theorem List (p. 233 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cnrm 23201 | Extend class notation with the class of all normal topologies. |
class Nrm | ||
Syntax | ccnrm 23202 | Extend class notation with the class of all completely normal topologies. |
class CNrm | ||
Syntax | cpnrm 23203 | Extend class notation with the class of all perfectly normal topologies. |
class PNrm | ||
Definition | df-t0 23204* | Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2698): any two points which are members of the same open sets are equal, or in contraposition, for any two distinct points there is an open set which contains one point but not the other. This differs from T1 spaces (see ist1-2 23238) in that in a T1 space you can choose which point will be in the open set and which outside; in a T0 space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ Kol2 = {π β Top β£ βπ₯ β βͺ πβπ¦ β βͺ π(βπ β π (π₯ β π β π¦ β π) β π₯ = π¦)} | ||
Definition | df-t1 23205* | The class of all T1 spaces, also called FrΓ©chet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.) |
β’ Fre = {π₯ β Top β£ βπ β βͺ π₯{π} β (Clsdβπ₯)} | ||
Definition | df-haus 23206* | Define the class of all Hausdorff (or T2) spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98. (Contributed by NM, 8-Mar-2007.) |
β’ Haus = {π β Top β£ βπ₯ β βͺ πβπ¦ β βͺ π(π₯ β π¦ β βπ β π βπ β π (π₯ β π β§ π¦ β π β§ (π β© π) = β ))} | ||
Definition | df-reg 23207* | Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ Reg = {π β Top β£ βπ₯ β π βπ¦ β π₯ βπ§ β π (π¦ β π§ β§ ((clsβπ)βπ§) β π₯)} | ||
Definition | df-nrm 23208* | Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ Nrm = {π β Top β£ βπ₯ β π βπ¦ β ((Clsdβπ) β© π« π₯)βπ§ β π (π¦ β π§ β§ ((clsβπ)βπ§) β π₯)} | ||
Definition | df-cnrm 23209* | Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ CNrm = {π β Top β£ βπ₯ β π« βͺ π(π βΎt π₯) β Nrm} | ||
Definition | df-pnrm 23210* | Define perfectly normal spaces. A space is perfectly normal if it is normal and every closed set is a Gδ set, meaning that it is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ PNrm = {π β Nrm β£ (Clsdβπ) β ran (π β (π βm β) β¦ β© ran π)} | ||
Theorem | ist0 23211* | The predicate "is a T0 space". Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 23236. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ (π½ β Kol2 β (π½ β Top β§ βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist1 23212* | The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.) |
β’ π = βͺ π½ β β’ (π½ β Fre β (π½ β Top β§ βπ β π {π} β (Clsdβπ½))) | ||
Theorem | ishaus 23213* | The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ (π½ β Haus β (π½ β Top β§ βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | iscnrm 23214* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β CNrm β (π½ β Top β§ βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | t0sep 23215* | Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π)) β (βπ₯ β π½ (π΄ β π₯ β π΅ β π₯) β π΄ = π΅)) | ||
Theorem | t0dist 23216* | Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ Β¬ (π΄ β π β π΅ β π)) | ||
Theorem | t1sncld 23217 | In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π) β {π΄} β (Clsdβπ½)) | ||
Theorem | t1ficld 23218 | In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΄ β Fin) β π΄ β (Clsdβπ½)) | ||
Theorem | hausnei 23219* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ (π β π β§ π β π β§ π β π)) β βπ β π½ βπ β π½ (π β π β§ π β π β§ (π β© π) = β )) | ||
Theorem | t0top 23220 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Kol2 β π½ β Top) | ||
Theorem | t1top 23221 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Top) | ||
Theorem | haustop 23222 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
β’ (π½ β Haus β π½ β Top) | ||
Theorem | isreg 23223* | The predicate "is a regular space". In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β Reg β (π½ β Top β§ βπ₯ β π½ βπ¦ β π₯ βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯))) | ||
Theorem | regtop 23224 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Reg β π½ β Top) | ||
Theorem | regsep 23225* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Reg β§ π β π½ β§ π΄ β π) β βπ₯ β π½ (π΄ β π₯ β§ ((clsβπ½)βπ₯) β π)) | ||
Theorem | isnrm 23226* | The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Nrm β (π½ β Top β§ βπ₯ β π½ βπ¦ β ((Clsdβπ½) β© π« π₯)βπ§ β π½ (π¦ β π§ β§ ((clsβπ½)βπ§) β π₯))) | ||
Theorem | nrmtop 23227 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Nrm β π½ β Top) | ||
Theorem | cnrmtop 23228 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Top) | ||
Theorem | iscnrm2 23229* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β CNrm β βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | ispnrm 23230* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β (π½ β Nrm β§ (Clsdβπ½) β ran (π β (π½ βm β) β¦ β© ran π))) | ||
Theorem | pnrmnrm 23231 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Nrm) | ||
Theorem | pnrmtop 23232 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Top) | ||
Theorem | pnrmcld 23233* | A closed set in a perfectly normal space is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β PNrm β§ π΄ β (Clsdβπ½)) β βπ β (π½ βm β)π΄ = β© ran π) | ||
Theorem | pnrmopn 23234* | An open set in a perfectly normal space is a countable union of closed sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β PNrm β§ π΄ β π½) β βπ β ((Clsdβπ½) βm β)π΄ = βͺ ran π) | ||
Theorem | ist0-2 23235* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist0-3 23236* | The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ ((π₯ β π β§ Β¬ π¦ β π) β¨ (Β¬ π₯ β π β§ π¦ β π))))) | ||
Theorem | cnt0 23237 | The preimage of a T0 topology under an injective map is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((πΎ β Kol2 β§ πΉ:πβ1-1βπ β§ πΉ β (π½ Cn πΎ)) β π½ β Kol2) | ||
Theorem | ist1-2 23238* | An alternate characterization of T1 spaces. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | t1t0 23239 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Kol2) | ||
Theorem | ist1-3 23240* | A space is T1 iff every point is the only point in the intersection of all open sets containing that point. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Fre β βπ₯ β π β© {π β π½ β£ π₯ β π} = {π₯})) | ||
Theorem | cnt1 23241 | The preimage of a T1 topology under an injective map is T1. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((πΎ β Fre β§ πΉ:πβ1-1βπ β§ πΉ β (π½ Cn πΎ)) β π½ β Fre) | ||
Theorem | ishaus2 23242* | Express the predicate "π½ is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | haust1 23243 | A Hausdorff space is a T1 space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Haus β π½ β Fre) | ||
Theorem | hausnei2 23244* | The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009.) |
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ’ β ((neiβπ½)β{π₯})βπ£ β ((neiβπ½)β{π¦})(π’ β© π£) = β ))) | ||
Theorem | cnhaus 23245 | The preimage of a Hausdorff topology under an injective map is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((πΎ β Haus β§ πΉ:πβ1-1βπ β§ πΉ β (π½ Cn πΎ)) β π½ β Haus) | ||
Theorem | nrmsep3 23246* | In a normal space, given a closed set π΅ inside an open set π΄, there is an open set π₯ such that π΅ β π₯ β cls(π₯) β π΄. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((π½ β Nrm β§ (π΄ β π½ β§ π΅ β (Clsdβπ½) β§ π΅ β π΄)) β βπ₯ β π½ (π΅ β π₯ β§ ((clsβπ½)βπ₯) β π΄)) | ||
Theorem | nrmsep2 23247* | In a normal space, any two disjoint closed sets have the property that each one is a subset of an open set whose closure is disjoint from the other. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ ((π½ β Nrm β§ (πΆ β (Clsdβπ½) β§ π· β (Clsdβπ½) β§ (πΆ β© π·) = β )) β βπ₯ β π½ (πΆ β π₯ β§ (((clsβπ½)βπ₯) β© π·) = β )) | ||
Theorem | nrmsep 23248* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ ((π½ β Nrm β§ (πΆ β (Clsdβπ½) β§ π· β (Clsdβπ½) β§ (πΆ β© π·) = β )) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β )) | ||
Theorem | isnrm2 23249* | An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma. (Contributed by Jeff Hankins, 1-Feb-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Nrm β (π½ β Top β§ βπ β (Clsdβπ½)βπ β (Clsdβπ½)((π β© π) = β β βπ β π½ (π β π β§ (((clsβπ½)βπ) β© π) = β )))) | ||
Theorem | isnrm3 23250* | A topological space is normal iff any two disjoint closed sets are separated by open sets. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β Nrm β (π½ β Top β§ βπ β (Clsdβπ½)βπ β (Clsdβπ½)((π β© π) = β β βπ₯ β π½ βπ¦ β π½ (π β π₯ β§ π β π¦ β§ (π₯ β© π¦) = β )))) | ||
Theorem | cnrmi 23251 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β Nrm) | ||
Theorem | cnrmnrm 23252 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Nrm) | ||
Theorem | restcnrm 23253 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β CNrm) | ||
Theorem | resthauslem 23254 | Lemma for resthaus 23259 and similar theorems. If the topological property π΄ is preserved under injective preimages, then property π΄ passes to subspaces. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β π΄ β π½ β Top) & β’ ((π½ β π΄ β§ ( I βΎ (π β© βͺ π½)):(π β© βͺ π½)β1-1β(π β© βͺ π½) β§ ( I βΎ (π β© βͺ π½)) β ((π½ βΎt π) Cn π½)) β (π½ βΎt π) β π΄) β β’ ((π½ β π΄ β§ π β π) β (π½ βΎt π) β π΄) | ||
Theorem | lpcls 23255 | The limit points of the closure of a subset are the same as the limit points of the set in a T1 space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π β π) β ((limPtβπ½)β((clsβπ½)βπ)) = ((limPtβπ½)βπ)) | ||
Theorem | perfcls 23256 | A subset of a perfect space is perfect iff its closure is perfect (and the closure is an actual perfect set, since it is both closed and perfect in the subspace topology). (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π β π) β ((π½ βΎt π) β Perf β (π½ βΎt ((clsβπ½)βπ)) β Perf)) | ||
Theorem | restt0 23257 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Kol2 β§ π΄ β π) β (π½ βΎt π΄) β Kol2) | ||
Theorem | restt1 23258 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Fre β§ π΄ β π) β (π½ βΎt π΄) β Fre) | ||
Theorem | resthaus 23259 | A subspace of a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Haus β§ π΄ β π) β (π½ βΎt π΄) β Haus) | ||
Theorem | t1sep2 23260* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΅ β π) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅)) | ||
Theorem | t1sep 23261* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ (π΄ β π β§ Β¬ π΅ β π)) | ||
Theorem | sncld 23262 | A singleton is closed in a Hausdorff space. (Contributed by NM, 5-Mar-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ π β π) β {π} β (Clsdβπ½)) | ||
Theorem | sshauslem 23263 | Lemma for sshaus 23266 and similar theorems. If the topological property π΄ is preserved under injective preimages, then a topology finer than one with property π΄ also has property π΄. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ & β’ (π½ β π΄ β π½ β Top) & β’ ((π½ β π΄ β§ ( I βΎ π):πβ1-1βπ β§ ( I βΎ π) β (πΎ Cn π½)) β πΎ β π΄) β β’ ((π½ β π΄ β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β π΄) | ||
Theorem | sst0 23264 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Kol2) | ||
Theorem | sst1 23265 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Fre) | ||
Theorem | sshaus 23266 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Haus) | ||
Theorem | regsep2 23267* | In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Reg β§ (πΆ β (Clsdβπ½) β§ π΄ β π β§ Β¬ π΄ β πΆ)) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π΄ β π¦ β§ (π₯ β© π¦) = β )) | ||
Theorem | isreg2 23268* | A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Reg β βπ β (Clsdβπ½)βπ₯ β π (Β¬ π₯ β π β βπ β π½ βπ β π½ (π β π β§ π₯ β π β§ (π β© π) = β )))) | ||
Theorem | dnsconst 23269 | If a continuous mapping to a T1 space is constant on a dense subset, it is constant on the entire space. Note that ((clsβπ½)βπ΄) = π means "π΄ is dense in π " and π΄ β (β‘πΉ β {π}) means "πΉ is constant on π΄ " (see funconstss 7059). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((πΎ β Fre β§ πΉ β (π½ Cn πΎ)) β§ (π β π β§ π΄ β (β‘πΉ β {π}) β§ ((clsβπ½)βπ΄) = π)) β πΉ:πβΆ{π}) | ||
Theorem | ordtt1 23270 | The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β PosetRel β (ordTopβπ ) β Fre) | ||
Theorem | lmmo 23271 | A sequence in a Hausdorff space converges to at most one limit. Part of Lemma 1.4-2(a) of [Kreyszig] p. 26. (Contributed by NM, 31-Jan-2008.) (Proof shortened by Mario Carneiro, 1-May-2014.) |
β’ (π β π½ β Haus) & β’ (π β πΉ(βπ‘βπ½)π΄) & β’ (π β πΉ(βπ‘βπ½)π΅) β β’ (π β π΄ = π΅) | ||
Theorem | lmfun 23272 | The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.) |
β’ (π½ β Haus β Fun (βπ‘βπ½)) | ||
Theorem | dishaus 23273 | A discrete topology is Hausdorff. Morris, Topology without tears, p.72, ex. 13. (Contributed by FL, 24-Jun-2007.) (Proof shortened by Mario Carneiro, 8-Apr-2015.) |
β’ (π΄ β π β π« π΄ β Haus) | ||
Theorem | ordthauslem 23274* | Lemma for ordthaus 23275. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ π = dom π β β’ ((π β TosetRel β§ π΄ β π β§ π΅ β π) β (π΄π π΅ β (π΄ β π΅ β βπ β (ordTopβπ )βπ β (ordTopβπ )(π΄ β π β§ π΅ β π β§ (π β© π) = β )))) | ||
Theorem | ordthaus 23275 | The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ (π β TosetRel β (ordTopβπ ) β Haus) | ||
Theorem | xrhaus 23276 | The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
β’ (ordTopβ β€ ) β Haus | ||
Syntax | ccmp 23277 | Extend class notation with the class of all compact spaces. |
class Comp | ||
Definition | df-cmp 23278* | Definition of a compact topology. A topology is compact iff any open covering of its underlying set contains a finite subcovering (Heine-Borel property). Definition C''' of [BourbakiTop1] p. I.59. Note: Bourbaki uses the term "quasi-compact" (saving "compact" for "compact Hausdorff"), but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008.) |
β’ Comp = {π₯ β Top β£ βπ¦ β π« π₯(βͺ π₯ = βͺ π¦ β βπ§ β (π« π¦ β© Fin)βͺ π₯ = βͺ π§)} | ||
Theorem | iscmp 23279* | The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ π = βͺ π½ β β’ (π½ β Comp β (π½ β Top β§ βπ¦ β π« π½(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | cmpcov 23280* | An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ π β π½ β§ π = βͺ π) β βπ β (π« π β© Fin)π = βͺ π ) | ||
Theorem | cmpcov2 23281* | Rewrite cmpcov 23280 for the cover {π¦ β π½ β£ π}. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ βπ₯ β π βπ¦ β π½ (π₯ β π¦ β§ π)) β βπ β (π« π½ β© Fin)(π = βͺ π β§ βπ¦ β π π)) | ||
Theorem | cmpcovf 23282* | Combine cmpcov 23280 with ac6sfi 9303 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 23283 | 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 23284 | A finite topology is compact. (Contributed by FL, 22-Dec-2008.) |
β’ (π½ β (Top β© Fin) β π½ β Comp) | ||
Theorem | 0cmp 23285 | The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.) |
β’ {β } β Comp | ||
Theorem | cmptop 23286 | A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ (π½ β Comp β π½ β Top) | ||
Theorem | rncmp 23287 | 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 23288 | 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 23289 | A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ (π΄ β Fin β π« π΄ β Comp) | ||
Theorem | cmpsublem 23290* | Lemma for cmpsub 23291. (Contributed by Jeff Hankins, 28-Jun-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (βπ β π« π½(π β βͺ π β βπ β (π« π β© Fin)π β βͺ π) β βπ β π« (π½ βΎt π)(βͺ (π½ βΎt π) = βͺ π β βπ‘ β (π« π β© Fin)βͺ (π½ βΎt π) = βͺ π‘))) | ||
Theorem | cmpsub 23291* | 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 23292* | A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23936, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π΅ β TopBases β§ π = βͺ π΅) β ((topGenβπ΅) β Comp β βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | cmpcld 23293 | A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ ((π½ β Comp β§ π β (Clsdβπ½)) β (π½ βΎt π) β Comp) | ||
Theorem | uncmp 23294 | The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π = (π βͺ π)) β§ ((π½ βΎt π) β Comp β§ (π½ βΎt π) β Comp)) β π½ β Comp) | ||
Theorem | fiuncmp 23295* | A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ βπ₯ β π΄ (π½ βΎt π΅) β Comp) β (π½ βΎt βͺ π₯ β π΄ π΅) β Comp) | ||
Theorem | sscmp 23296 | 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 23297* | Lemma for hauscmp 23298. (Contributed by Mario Carneiro, 27-Nov-2013.) |
β’ π = βͺ π½ & β’ π = {π¦ β π½ β£ βπ€ β π½ (π΄ β π€ β§ ((clsβπ½)βπ€) β (π β π¦))} & β’ (π β π½ β Haus) & β’ (π β π β π) & β’ (π β (π½ βΎt π) β Comp) & β’ (π β π΄ β (π β π)) β β’ (π β βπ§ β π½ (π΄ β π§ β§ ((clsβπ½)βπ§) β (π β π))) | ||
Theorem | hauscmp 23298 | 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 23299* | 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 23300 | 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βπ)) β β© π β β ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |