![]() |
Metamath
Proof Explorer Theorem List (p. 234 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48421) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hausnei2 23301* | 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 23302 | 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 23303* | 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 23304* | 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 23305* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ ((𝐽 ∈ Nrm ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐷 ∈ (Clsd‘𝐽) ∧ (𝐶 ∩ 𝐷) = ∅)) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | isnrm2 23306* | 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 23307* | 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 23308 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Nrm) | ||
Theorem | cnrmnrm 23309 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Nrm) | ||
Theorem | restcnrm 23310 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ CNrm) | ||
Theorem | resthauslem 23311 | Lemma for resthaus 23316 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 23312 | 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 23313 | 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 23314 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Kol2 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Kol2) | ||
Theorem | restt1 23315 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Fre) | ||
Theorem | resthaus 23316 | 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 23317* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → 𝐴 = 𝐵)) | ||
Theorem | t1sep 23318* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜)) | ||
Theorem | sncld 23319 | 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 23320 | Lemma for sshaus 23323 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 23321 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Kol2 ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Kol2) | ||
Theorem | sst1 23322 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Fre) | ||
Theorem | sshaus 23323 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Haus) | ||
Theorem | regsep2 23324* | 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 23325* | 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 23326 | 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 7064). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐾 ∈ Fre ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ (◡𝐹 “ {𝑃}) ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐹:𝑋⟶{𝑃}) | ||
Theorem | ordtt1 23327 | The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ Fre) | ||
Theorem | lmmo 23328 | 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 23329 | The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ (𝐽 ∈ Haus → Fun (⇝𝑡‘𝐽)) | ||
Theorem | dishaus 23330 | 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 23331* | Lemma for ordthaus 23332. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → (𝐴 ≠ 𝐵 → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)))) | ||
Theorem | ordthaus 23332 | The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ (𝑅 ∈ TosetRel → (ordTop‘𝑅) ∈ Haus) | ||
Theorem | xrhaus 23333 | The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ (ordTop‘ ≤ ) ∈ Haus | ||
Syntax | ccmp 23334 | Extend class notation with the class of all compact spaces. |
class Comp | ||
Definition | df-cmp 23335* | 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 23336* | The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) | ||
Theorem | cmpcov 23337* | An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆) → ∃𝑠 ∈ (𝒫 𝑆 ∩ Fin)𝑋 = ∪ 𝑠) | ||
Theorem | cmpcov2 23338* | Rewrite cmpcov 23337 for the cover {𝑦 ∈ 𝐽 ∣ 𝜑}. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∃𝑠 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑠 ∧ ∀𝑦 ∈ 𝑠 𝜑)) | ||
Theorem | cmpcovf 23339* | Combine cmpcov 23337 with ac6sfi 9312 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 23340 | 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 23341 | A finite topology is compact. (Contributed by FL, 22-Dec-2008.) |
⊢ (𝐽 ∈ (Top ∩ Fin) → 𝐽 ∈ Comp) | ||
Theorem | 0cmp 23342 | The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.) |
⊢ {∅} ∈ Comp | ||
Theorem | cmptop 23343 | A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.) |
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) | ||
Theorem | rncmp 23344 | 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 23345 | 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 23346 | A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Comp) | ||
Theorem | cmpsublem 23347* | Lemma for cmpsub 23348. (Contributed by Jeff Hankins, 28-Jun-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) | ||
Theorem | cmpsub 23348* | 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 23349* | A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23993, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) | ||
Theorem | cmpcld 23350 | A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.) |
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp) | ||
Theorem | uncmp 23351 | The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp) | ||
Theorem | fiuncmp 23352* | A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp) | ||
Theorem | sscmp 23353 | 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 23354* | Lemma for hauscmp 23355. (Contributed by Mario Carneiro, 27-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} & ⊢ (𝜑 → 𝐽 ∈ Haus) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp) & ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆)) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | ||
Theorem | hauscmp 23355 | 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 23356* | 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 23357 | 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 23358* | 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 23359 | Extend class notation with the class of all connected topologies. |
class Conn | ||
Definition | df-conn 23360 | Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.) |
⊢ Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} | ||
Theorem | isconn 23361 | The predicate 𝐽 is a connected topology . (Contributed by FL, 17-Nov-2008.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) = {∅, 𝑋})) | ||
Theorem | isconn2 23362 | The predicate 𝐽 is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝑋})) | ||
Theorem | connclo 23363 | The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Conn) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → 𝐴 = 𝑋) | ||
Theorem | conndisj 23364 | 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 23365 | A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.) |
⊢ (𝐽 ∈ Conn → 𝐽 ∈ Top) | ||
Theorem | indisconn 23366 | 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 23367* | An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋))) | ||
Theorem | connsuba 23368* | Connectedness for a subspace. See connsub 23369. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐽 ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝐴) ≠ ∅ ∧ (𝑦 ∩ 𝐴) ≠ ∅ ∧ ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) → ((𝑥 ∪ 𝑦) ∩ 𝐴) ≠ 𝐴))) | ||
Theorem | connsub 23369* | 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 23370 | 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 23371 | Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → (𝑈 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → (𝑉 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → ((𝑈 ∩ 𝑉) ∩ 𝐴) = ∅) & ⊢ (𝜑 → 𝐴 ⊆ (𝑈 ∪ 𝑉)) ⇒ ⊢ (𝜑 → ¬ (𝐽 ↾t 𝐴) ∈ Conn) | ||
Theorem | connsubclo 23372 | 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 23373 | 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 23374 | 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 23375* | Lemma for iunconn 23376. (Contributed by Mario Carneiro, 11-Jun-2014.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → (𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) & ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵)) & ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉)) & ⊢ Ⅎ𝑘𝜑 ⇒ ⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈) | ||
Theorem | iunconn 23376* | 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 23377 | 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 23378 | The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Conn) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Conn) | ||
Theorem | conncompid 23379* | The connected component containing 𝐴 contains 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑆) | ||
Theorem | conncompconn 23380* | The connected component containing 𝐴 is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn) | ||
Theorem | conncompss 23381* | 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 23382* | The connected component containing 𝐴 is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | conncompclo 23383* | 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 23384 | 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 23385 | Extend class definition to include the class of all first-countable topologies. |
class 1stω | ||
Syntax | c2ndc 23386 | Extend class definition to include the class of all second-countable topologies. |
class 2ndω | ||
Definition | df-1stc 23387* | Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))} | ||
Definition | df-2ndc 23388* | Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.) |
⊢ 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)} | ||
Theorem | is1stc 23389* | 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 23390* | 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 23391 | A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top) | ||
Theorem | 1stcclb 23392* | A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑧 ∈ 𝑥 (𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)))) | ||
Theorem | 1stcfb 23393* | 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 23394* | 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 23395 | 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 23396 | A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ≼ ω) → (topGen‘𝐵) ∈ 2ndω) | ||
Theorem | 2ndcsb 23397* | 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 23398 | A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐽 ∈ 2ndω → 𝐽 ≼ ℝ) | ||
Theorem | 2ndc1stc 23399 | A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) |
⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ 1stω) | ||
Theorem | 1stcrestlem 23400* | Lemma for 1stcrest 23401. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |