Home | Metamath
Proof Explorer Theorem List (p. 219 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnima 21801 | An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) | ||
Theorem | cnco 21802 | The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐿)) → (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐿)) | ||
Theorem | cnpco 21803 | The composition of a function 𝐹 continuous at 𝑃 with a function continuous at (𝐹‘𝑃) is continuous at 𝑃. Proposition 2 of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)‘𝑃)) | ||
Theorem | cnclima 21804 | A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽)) | ||
Theorem | iscncl 21805* | A characterization of a continuity function using closed sets. Theorem 1(d) of [BourbakiTop1] p. I.9. (Contributed by FL, 19-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) | ||
Theorem | cncls2i 21806 | Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐽)‘(◡𝐹 “ 𝑆)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑆))) | ||
Theorem | cnntri 21807 | Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → (◡𝐹 “ ((int‘𝐾)‘𝑆)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑆))) | ||
Theorem | cnclsi 21808 | Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆))) | ||
Theorem | cncls2 21809* | Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑌((cls‘𝐽)‘(◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑥))))) | ||
Theorem | cncls 21810* | Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑋(𝐹 “ ((cls‘𝐽)‘𝑥)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑥))))) | ||
Theorem | cnntr 21811* | Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑌(◡𝐹 “ ((int‘𝐾)‘𝑥)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑥))))) | ||
Theorem | cnss1 21812 | If the topology 𝐾 is finer than 𝐽, then there are more continuous functions from 𝐾 than from 𝐽. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐽 Cn 𝐿) ⊆ (𝐾 Cn 𝐿)) | ||
Theorem | cnss2 21813 | If the topology 𝐾 is finer than 𝐽, then there are fewer continuous functions into 𝐾 than into 𝐽 from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐿 ∈ (TopOn‘𝑌) ∧ 𝐿 ⊆ 𝐾) → (𝐽 Cn 𝐾) ⊆ (𝐽 Cn 𝐿)) | ||
Theorem | cncnpi 21814 | A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) | ||
Theorem | cnsscnp 21815 | The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑃 ∈ 𝑋 → (𝐽 Cn 𝐾) ⊆ ((𝐽 CnP 𝐾)‘𝑃)) | ||
Theorem | cncnp 21816* | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))) | ||
Theorem | cncnp2 21817* | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝑋 ≠ ∅ → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) | ||
Theorem | cnnei 21818* | Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑝 ∈ 𝑋 ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑝)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑝})(𝐹 “ 𝑣) ⊆ 𝑤)) | ||
Theorem | cnconst2 21819 | A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ 𝑌) → (𝑋 × {𝐵}) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnconst 21820 | A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐵 ∈ 𝑌 ∧ 𝐹:𝑋⟶{𝐵})) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnrest 21821 | Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) | ||
Theorem | cnrest2 21822 | Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)))) | ||
Theorem | cnrest2r 21823 | Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝐾 ∈ Top → (𝐽 Cn (𝐾 ↾t 𝐵)) ⊆ (𝐽 Cn 𝐾)) | ||
Theorem | cnpresti 21824 | One direction of cnprest 21825 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑃 ∈ 𝐴 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹 ↾ 𝐴) ∈ (((𝐽 ↾t 𝐴) CnP 𝐾)‘𝑃)) | ||
Theorem | cnprest 21825 | 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 21826 | 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 21827 | 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 𝐽) = (𝑋 ↑m 𝐴)) | ||
Theorem | cnindis 21828 | 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 {∅, 𝐴}) = (𝐴 ↑m 𝑋)) | ||
Theorem | cnpdis 21829 | 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 𝐾)‘𝐴) = (𝑌 ↑m 𝑋)) | ||
Theorem | paste 21830 | 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 21831 | If 𝐹 converges, then 𝐹 is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ∈ (𝑋 ↑pm ℂ)) | ||
Theorem | lmfss 21832 | 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 21833 | Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ 𝑋) | ||
Theorem | lmss 21834 | Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
⊢ 𝐾 = (𝐽 ↾t 𝑌) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑃 ∈ 𝑌) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑌) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃)) | ||
Theorem | sslm 21835 | 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 21836 | A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm ℂ)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ↾ (ℤ≥‘𝑀))(⇝𝑡‘𝐽)𝑃)) | ||
Theorem | lmff 21837* | 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 21838* | 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 21839* | 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 21840 | 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 21841 | 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 21842 | Extend class notation with the class of all T0 spaces. |
class Kol2 | ||
Syntax | ct1 21843 | Extend class notation to include T1 spaces (also called Fréchet spaces). |
class Fre | ||
Syntax | cha 21844 | Extend class notation with the class of all Hausdorff spaces. |
class Haus | ||
Syntax | creg 21845 | Extend class notation with the class of all regular topologies. |
class Reg | ||
Syntax | cnrm 21846 | Extend class notation with the class of all normal topologies. |
class Nrm | ||
Syntax | ccnrm 21847 | Extend class notation with the class of all completely normal topologies. |
class CNrm | ||
Syntax | cpnrm 21848 | Extend class notation with the class of all perfectly normal topologies. |
class PNrm | ||
Definition | df-t0 21849* | Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2790): 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 21883) 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 21850* | 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 21851* | 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 21852* | 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 21853* | 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 21854* | 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 21855* | 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 21856* | 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 21881. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) | ||
Theorem | ist1 21857* | The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Fre ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 {𝑎} ∈ (Clsd‘𝐽))) | ||
Theorem | ishaus 21858* | The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) | ||
Theorem | iscnrm 21859* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ CNrm ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm)) | ||
Theorem | t0sep 21860* | Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥) → 𝐴 = 𝐵)) | ||
Theorem | t0dist 21861* | Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 ¬ (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜)) | ||
Theorem | t1sncld 21862 | In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋) → {𝐴} ∈ (Clsd‘𝐽)) | ||
Theorem | t1ficld 21863 | In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | hausnei 21864* | Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑃 ≠ 𝑄)) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) | ||
Theorem | t0top 21865 | A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Kol2 → 𝐽 ∈ Top) | ||
Theorem | t1top 21866 | A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Top) | ||
Theorem | haustop 21867 | A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) | ||
Theorem | isreg 21868* | 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 21869 | A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Reg → 𝐽 ∈ Top) | ||
Theorem | regsep 21870* | In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Reg ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ ((cls‘𝐽)‘𝑥) ⊆ 𝑈)) | ||
Theorem | isnrm 21871* | 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 21872 | A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top) | ||
Theorem | cnrmtop 21873 | A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Top) | ||
Theorem | iscnrm2 21874* | The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ CNrm ↔ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm)) | ||
Theorem | ispnrm 21875* | The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ PNrm ↔ (𝐽 ∈ Nrm ∧ (Clsd‘𝐽) ⊆ ran (𝑓 ∈ (𝐽 ↑m ℕ) ↦ ∩ ran 𝑓))) | ||
Theorem | pnrmnrm 21876 | A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Nrm) | ||
Theorem | pnrmtop 21877 | A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Top) | ||
Theorem | pnrmcld 21878* | 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 21879* | 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 21880* | The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦))) | ||
Theorem | ist0-3 21881* | The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑜 ∈ 𝐽 ((𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜) ∨ (¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜))))) | ||
Theorem | cnt0 21882 | 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 21883* | 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 21884 | A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Kol2) | ||
Theorem | ist1-3 21885* | 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 21886 | 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 21887* | Express the predicate "𝐽 is a Hausdorff space." (Contributed by NM, 8-Mar-2007.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) | ||
Theorem | haust1 21888 | 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 21889* | 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 21890 | 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 21891* | 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 21892* | 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 21893* | In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.) |
⊢ ((𝐽 ∈ Nrm ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐷 ∈ (Clsd‘𝐽) ∧ (𝐶 ∩ 𝐷) = ∅)) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | isnrm2 21894* | 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 21895* | 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 21896 | A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Nrm) | ||
Theorem | cnrmnrm 21897 | A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Nrm) | ||
Theorem | restcnrm 21898 | A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ CNrm) | ||
Theorem | resthauslem 21899 | Lemma for resthaus 21904 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 21900 | 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‘𝐽)‘𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |