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