![]() |
Metamath
Proof Explorer Theorem List (p. 216 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnprest 21501 | Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ (𝑃 ∈ ((int‘𝐽)‘𝐴) ∧ 𝐹:𝑋⟶𝑌)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃))) | ||
Theorem | cnprest2 21502 | Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃))) | ||
Theorem | cndis 21503 | Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝒫 𝐴 Cn 𝐽) = (𝑋 ↑𝑚 𝐴)) | ||
Theorem | cnindis 21504 | Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 Cn {∅, 𝐴}) = (𝐴 ↑𝑚 𝑋)) | ||
Theorem | cnpdis 21505 | If 𝐴 is an isolated point in 𝑋 (or equivalently, the singleton {𝐴} is open in 𝑋), then every function is continuous at 𝐴. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → ((𝐽 CnP 𝐾)‘𝐴) = (𝑌 ↑𝑚 𝑋)) | ||
Theorem | paste 21506 | Pasting lemma. If 𝐴 and 𝐵 are closed sets in 𝑋 with 𝐴 ∪ 𝐵 = 𝑋, then any function whose restrictions to 𝐴 and 𝐵 are continuous is continuous on all of 𝑋. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝑋) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) & ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ ((𝐽 ↾t 𝐵) Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | lmfpm 21507 | If 𝐹 converges, then 𝐹 is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ∈ (𝑋 ↑pm ℂ)) | ||
Theorem | lmfss 21508 | Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ⊆ (ℂ × 𝑋)) | ||
Theorem | lmcl 21509 | Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ 𝑋) | ||
Theorem | lmss 21510 | Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
⊢ 𝐾 = (𝐽 ↾t 𝑌) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑃 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑌) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)) | ||
Theorem | sslm 21511 | A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (⇝𝑡‘𝐾) ⊆ (⇝𝑡‘𝐽)) | ||
Theorem | lmres 21512 | A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm ℂ)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ↾ (ℤ≥‘𝑀))(⇝𝑡‘𝐽)𝑃)) | ||
Theorem | lmff 21513* | If 𝐹 converges, there is some upper integer set on which 𝐹 is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶𝑋) | ||
Theorem | lmcls 21514* | Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 𝑃 ∈ ((cls‘𝐽)‘𝑆)) | ||
Theorem | lmcld 21515* | Any convergent sequence of points in a closed subset of a topological space converges to a point in the set. (Contributed by Mario Carneiro, 30-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → 𝑃 ∈ 𝑆) | ||
Theorem | lmcnp 21516 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) |
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃)) | ||
Theorem | lmcn 21517 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) |
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃)) | ||
Syntax | ct0 21518 | Extend class notation with the class of all T0 spaces. |
class Kol2 | ||
Syntax | ct1 21519 | Extend class notation to include T1 spaces (also called Fréchet spaces). |
class Fre | ||
Syntax | cha 21520 | Extend class notation with the class of all Hausdorff spaces. |
class Haus | ||
Syntax | creg 21521 | Extend class notation with the class of all regular topologies. |
class Reg | ||
Syntax | cnrm 21522 | Extend class notation with the class of all normal topologies. |
class Nrm | ||
Syntax | ccnrm 21523 | Extend class notation with the class of all completely normal topologies. |
class CNrm | ||
Syntax | cpnrm 21524 | Extend class notation with the class of all perfectly normal topologies. |
class PNrm | ||
Definition | df-t0 21525* | Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2754): 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 21559) 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 21526* | 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 21527* | 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 21528* | 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 21529* | 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 21530* | 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 21531* | 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 (𝑓 ∈ (𝑗 ↑𝑚 ℕ) ↦ ∩ ran 𝑓)} | ||
Theorem | ist0 21532* | 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 21557. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) | ||
Theorem | ist1 21533* | The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Fre ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 {𝑎} ∈ (Clsd‘𝐽))) | ||
Theorem | ishaus 21534* | The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) | ||
Theorem | iscnrm 21535* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ CNrm ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm)) | ||
Theorem | t0sep 21536* | Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥) → 𝐴 = 𝐵)) | ||
Theorem | t0dist 21537* | Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 ¬ (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜)) | ||
Theorem | t1sncld 21538 | In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋) → {𝐴} ∈ (Clsd‘𝐽)) | ||
Theorem | t1ficld 21539 | In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | hausnei 21540* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑃 ≠ 𝑄)) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) | ||
Theorem | t0top 21541 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Kol2 → 𝐽 ∈ Top) | ||
Theorem | t1top 21542 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Top) | ||
Theorem | haustop 21543 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) | ||
Theorem | isreg 21544* | 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 21545 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Reg → 𝐽 ∈ Top) | ||
Theorem | regsep 21546* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Reg ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ ((cls‘𝐽)‘𝑥) ⊆ 𝑈)) | ||
Theorem | isnrm 21547* | 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 21548 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top) | ||
Theorem | cnrmtop 21549 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Top) | ||
Theorem | iscnrm2 21550* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ CNrm ↔ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm)) | ||
Theorem | ispnrm 21551* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ PNrm ↔ (𝐽 ∈ Nrm ∧ (Clsd‘𝐽) ⊆ ran (𝑓 ∈ (𝐽 ↑𝑚 ℕ) ↦ ∩ ran 𝑓))) | ||
Theorem | pnrmnrm 21552 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Nrm) | ||
Theorem | pnrmtop 21553 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Top) | ||
Theorem | pnrmcld 21554* | A closed set in a perfectly normal space is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ PNrm ∧ 𝐴 ∈ (Clsd‘𝐽)) → ∃𝑓 ∈ (𝐽 ↑𝑚 ℕ)𝐴 = ∩ ran 𝑓) | ||
Theorem | pnrmopn 21555* | An open set in a perfectly normal space is a countable union of closed sets. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ PNrm ∧ 𝐴 ∈ 𝐽) → ∃𝑓 ∈ ((Clsd‘𝐽) ↑𝑚 ℕ)𝐴 = ∪ ran 𝑓) | ||
Theorem | ist0-2 21556* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) | ||
Theorem | ist0-3 21557* | The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑜 ∈ 𝐽 ((𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜) ∨ (¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜))))) | ||
Theorem | cnt0 21558 | 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 21559* | 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 21560 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Kol2) | ||
Theorem | ist1-3 21561* | 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 21562 | 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 21563* | Express the predicate "𝐽 is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) | ||
Theorem | haust1 21564 | 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 21565* | 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 21566 | 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 21567* | 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 21568* | 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 21569* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ ((𝐽 ∈ Nrm ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐷 ∈ (Clsd‘𝐽) ∧ (𝐶 ∩ 𝐷) = ∅)) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | isnrm2 21570* | 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 21571* | 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 21572 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Nrm) | ||
Theorem | cnrmnrm 21573 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Nrm) | ||
Theorem | restcnrm 21574 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ CNrm) | ||
Theorem | resthauslem 21575 | Lemma for resthaus 21580 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 21576 | 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 21577 | 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 21578 | A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Kol2 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Kol2) | ||
Theorem | restt1 21579 | A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Fre) | ||
Theorem | resthaus 21580 | 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 21581* | Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → 𝐴 = 𝐵)) | ||
Theorem | t1sep 21582* | Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜)) | ||
Theorem | sncld 21583 | 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 21584 | Lemma for sshaus 21587 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 21585 | A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Kol2 ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Kol2) | ||
Theorem | sst1 21586 | A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Fre) | ||
Theorem | sshaus 21587 | A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Haus) | ||
Theorem | regsep2 21588* | 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 21589* | 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 21590 | 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 6598). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐾 ∈ Fre ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ (◡𝐹 “ {𝑃}) ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐹:𝑋⟶{𝑃}) | ||
Theorem | ordtt1 21591 | The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ Fre) | ||
Theorem | lmmo 21592 | 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 21593 | The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ (𝐽 ∈ Haus → Fun (⇝𝑡‘𝐽)) | ||
Theorem | dishaus 21594 | 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 21595* | Lemma for ordthaus 21596. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → (𝐴 ≠ 𝐵 → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)))) | ||
Theorem | ordthaus 21596 | The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ (𝑅 ∈ TosetRel → (ordTop‘𝑅) ∈ Haus) | ||
Theorem | xrhaus 21597 | The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ (ordTop‘ ≤ ) ∈ Haus | ||
Syntax | ccmp 21598 | Extend class notation with the class of all compact spaces. |
class Comp | ||
Definition | df-cmp 21599* | 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" but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008.) |
⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)} | ||
Theorem | iscmp 21600* | The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |