Home | Metamath
Proof Explorer Theorem List (p. 227 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 | hausnei 22601* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ (π β π β§ π β π β§ π β π)) β βπ β π½ βπ β π½ (π β π β§ π β π β§ (π β© π) = β )) | ||
Theorem | t0top 22602 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Kol2 β π½ β Top) | ||
Theorem | t1top 22603 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Top) | ||
Theorem | haustop 22604 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
β’ (π½ β Haus β π½ β Top) | ||
Theorem | isreg 22605* | 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 22606 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Reg β π½ β Top) | ||
Theorem | regsep 22607* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Reg β§ π β π½ β§ π΄ β π) β βπ₯ β π½ (π΄ β π₯ β§ ((clsβπ½)βπ₯) β π)) | ||
Theorem | isnrm 22608* | 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 22609 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Nrm β π½ β Top) | ||
Theorem | cnrmtop 22610 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Top) | ||
Theorem | iscnrm2 22611* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β CNrm β βπ₯ β π« π(π½ βΎt π₯) β Nrm)) | ||
Theorem | ispnrm 22612* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β (π½ β Nrm β§ (Clsdβπ½) β ran (π β (π½ βm β) β¦ β© ran π))) | ||
Theorem | pnrmnrm 22613 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Nrm) | ||
Theorem | pnrmtop 22614 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β PNrm β π½ β Top) | ||
Theorem | pnrmcld 22615* | 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 22616* | 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 22617* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (βπ β π½ (π₯ β π β π¦ β π) β π₯ = π¦))) | ||
Theorem | ist0-3 22618* | The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ ((π₯ β π β§ Β¬ π¦ β π) β¨ (Β¬ π₯ β π β§ π¦ β π))))) | ||
Theorem | cnt0 22619 | 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 22620* | 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 22621 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ (π½ β Fre β π½ β Kol2) | ||
Theorem | ist1-3 22622* | 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 22623 | 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 22624* | Express the predicate "π½ is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
β’ (π½ β (TopOnβπ) β (π½ β Haus β βπ₯ β π βπ¦ β π (π₯ β π¦ β βπ β π½ βπ β π½ (π₯ β π β§ π¦ β π β§ (π β© π) = β )))) | ||
Theorem | haust1 22625 | 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 22626* | 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 22627 | 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 22628* | 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 22629* | 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 22630* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ ((π½ β Nrm β§ (πΆ β (Clsdβπ½) β§ π· β (Clsdβπ½) β§ (πΆ β© π·) = β )) β βπ₯ β π½ βπ¦ β π½ (πΆ β π₯ β§ π· β π¦ β§ (π₯ β© π¦) = β )) | ||
Theorem | isnrm2 22631* | 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 22632* | 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 22633 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β Nrm) | ||
Theorem | cnrmnrm 22634 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π½ β CNrm β π½ β Nrm) | ||
Theorem | restcnrm 22635 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β CNrm β§ π΄ β π) β (π½ βΎt π΄) β CNrm) | ||
Theorem | resthauslem 22636 | Lemma for resthaus 22641 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 22637 | 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 22638 | 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 22639 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Kol2 β§ π΄ β π) β (π½ βΎt π΄) β Kol2) | ||
Theorem | restt1 22640 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Fre β§ π΄ β π) β (π½ βΎt π΄) β Fre) | ||
Theorem | resthaus 22641 | 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 22642* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ π΄ β π β§ π΅ β π) β (βπ β π½ (π΄ β π β π΅ β π) β π΄ = π΅)) | ||
Theorem | t1sep 22643* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ (π΄ β π β§ π΅ β π β§ π΄ β π΅)) β βπ β π½ (π΄ β π β§ Β¬ π΅ β π)) | ||
Theorem | sncld 22644 | 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 22645 | Lemma for sshaus 22648 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 22646 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Kol2 β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Kol2) | ||
Theorem | sst1 22647 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Fre β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Fre) | ||
Theorem | sshaus 22648 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β πΎ β Haus) | ||
Theorem | regsep2 22649* | 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 22650* | 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 22651 | 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 7002). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((πΎ β Fre β§ πΉ β (π½ Cn πΎ)) β§ (π β π β§ π΄ β (β‘πΉ β {π}) β§ ((clsβπ½)βπ΄) = π)) β πΉ:πβΆ{π}) | ||
Theorem | ordtt1 22652 | The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β PosetRel β (ordTopβπ ) β Fre) | ||
Theorem | lmmo 22653 | 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 22654 | The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.) |
β’ (π½ β Haus β Fun (βπ‘βπ½)) | ||
Theorem | dishaus 22655 | 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 22656* | Lemma for ordthaus 22657. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ π = dom π β β’ ((π β TosetRel β§ π΄ β π β§ π΅ β π) β (π΄π π΅ β (π΄ β π΅ β βπ β (ordTopβπ )βπ β (ordTopβπ )(π΄ β π β§ π΅ β π β§ (π β© π) = β )))) | ||
Theorem | ordthaus 22657 | The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ (π β TosetRel β (ordTopβπ ) β Haus) | ||
Theorem | xrhaus 22658 | The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
β’ (ordTopβ β€ ) β Haus | ||
Syntax | ccmp 22659 | Extend class notation with the class of all compact spaces. |
class Comp | ||
Definition | df-cmp 22660* | 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 22661* | The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ π = βͺ π½ β β’ (π½ β Comp β (π½ β Top β§ βπ¦ β π« π½(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | cmpcov 22662* | An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ π β π½ β§ π = βͺ π) β βπ β (π« π β© Fin)π = βͺ π ) | ||
Theorem | cmpcov2 22663* | Rewrite cmpcov 22662 for the cover {π¦ β π½ β£ π}. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ βπ₯ β π βπ¦ β π½ (π₯ β π¦ β§ π)) β βπ β (π« π½ β© Fin)(π = βͺ π β§ βπ¦ β π π)) | ||
Theorem | cmpcovf 22664* | Combine cmpcov 22662 with ac6sfi 9165 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 22665 | 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 22666 | A finite topology is compact. (Contributed by FL, 22-Dec-2008.) |
β’ (π½ β (Top β© Fin) β π½ β Comp) | ||
Theorem | 0cmp 22667 | The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.) |
β’ {β } β Comp | ||
Theorem | cmptop 22668 | A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ (π½ β Comp β π½ β Top) | ||
Theorem | rncmp 22669 | 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 22670 | 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 22671 | A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ (π΄ β Fin β π« π΄ β Comp) | ||
Theorem | cmpsublem 22672* | Lemma for cmpsub 22673. (Contributed by Jeff Hankins, 28-Jun-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (βπ β π« π½(π β βͺ π β βπ β (π« π β© Fin)π β βͺ π) β βπ β π« (π½ βΎt π)(βͺ (π½ βΎt π) = βͺ π β βπ‘ β (π« π β© Fin)βͺ (π½ βΎt π) = βͺ π‘))) | ||
Theorem | cmpsub 22673* | 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 22674* | A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23318, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π΅ β TopBases β§ π = βͺ π΅) β ((topGenβπ΅) β Comp β βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | cmpcld 22675 | A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.) |
β’ ((π½ β Comp β§ π β (Clsdβπ½)) β (π½ βΎt π) β Comp) | ||
Theorem | uncmp 22676 | The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π = (π βͺ π)) β§ ((π½ βΎt π) β Comp β§ (π½ βΎt π) β Comp)) β π½ β Comp) | ||
Theorem | fiuncmp 22677* | A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ βπ₯ β π΄ (π½ βΎt π΅) β Comp) β (π½ βΎt βͺ π₯ β π΄ π΅) β Comp) | ||
Theorem | sscmp 22678 | 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 22679* | Lemma for hauscmp 22680. (Contributed by Mario Carneiro, 27-Nov-2013.) |
β’ π = βͺ π½ & β’ π = {π¦ β π½ β£ βπ€ β π½ (π΄ β π€ β§ ((clsβπ½)βπ€) β (π β π¦))} & β’ (π β π½ β Haus) & β’ (π β π β π) & β’ (π β (π½ βΎt π) β Comp) & β’ (π β π΄ β (π β π)) β β’ (π β βπ§ β π½ (π΄ β π§ β§ ((clsβπ½)βπ§) β (π β π))) | ||
Theorem | hauscmp 22680 | 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 22681* | 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 22682 | 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 22683* | 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 22684 | Extend class notation with the class of all connected topologies. |
class Conn | ||
Definition | df-conn 22685 | Topologies are connected when only β and βͺ π are both open and closed. (Contributed by FL, 17-Nov-2008.) |
β’ Conn = {π β Top β£ (π β© (Clsdβπ)) = {β , βͺ π}} | ||
Theorem | isconn 22686 | The predicate π½ is a connected topology . (Contributed by FL, 17-Nov-2008.) |
β’ π = βͺ π½ β β’ (π½ β Conn β (π½ β Top β§ (π½ β© (Clsdβπ½)) = {β , π})) | ||
Theorem | isconn2 22687 | The predicate π½ is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π = βͺ π½ β β’ (π½ β Conn β (π½ β Top β§ (π½ β© (Clsdβπ½)) β {β , π})) | ||
Theorem | connclo 22688 | The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π = βͺ π½ & β’ (π β π½ β Conn) & β’ (π β π΄ β π½) & β’ (π β π΄ β β ) & β’ (π β π΄ β (Clsdβπ½)) β β’ (π β π΄ = π) | ||
Theorem | conndisj 22689 | 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 22690 | A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.) |
β’ (π½ β Conn β π½ β Top) | ||
Theorem | indisconn 22691 | 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 22692* | An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Conn β βπ₯ β π½ βπ¦ β π½ ((π₯ β β β§ π¦ β β β§ (π₯ β© π¦) = β ) β (π₯ βͺ π¦) β π))) | ||
Theorem | connsuba 22693* | Connectedness for a subspace. See connsub 22694. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ((π½ βΎt π΄) β Conn β βπ₯ β π½ βπ¦ β π½ (((π₯ β© π΄) β β β§ (π¦ β© π΄) β β β§ ((π₯ β© π¦) β© π΄) = β ) β ((π₯ βͺ π¦) β© π΄) β π΄))) | ||
Theorem | connsub 22694* | 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 22695 | 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 22696 | Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β π) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β (π β© π΄) β β ) & β’ (π β (π β© π΄) β β ) & β’ (π β ((π β© π) β© π΄) = β ) & β’ (π β π΄ β (π βͺ π)) β β’ (π β Β¬ (π½ βΎt π΄) β Conn) | ||
Theorem | connsubclo 22697 | 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 22698 | 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 22699 | 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 22700* | Lemma for iunconn 22701. (Contributed by Mario Carneiro, 11-Jun-2014.) |
β’ (π β π½ β (TopOnβπ)) & β’ ((π β§ π β π΄) β π΅ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ ((π β§ π β π΄) β (π½ βΎt π΅) β Conn) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β (π β© βͺ π β π΄ π΅) β β ) & β’ (π β (π β© π) β (π β βͺ π β π΄ π΅)) & β’ (π β βͺ π β π΄ π΅ β (π βͺ π)) & β’ β²ππ β β’ (π β Β¬ π β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |