P. 237 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23601-23700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tgcnp 23601*	The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 = (topGen‘𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
Theorem	subbascn 23602*	The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐾 = (topGen‘(fi‘𝐵)))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)))
Theorem	ssidcn 23603	The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (( I ↾ 𝑋) ∈ (𝐽 Cn 𝐾) ↔ 𝐾 ⊆ 𝐽))
Theorem	cnpimaex 23604*	Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.)
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝐴) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝐴))
Theorem	idcn 23605	A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽))
Theorem	lmbr 23606*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23577. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢))))
Theorem	lmbr2 23607*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))))
Theorem	lmbrf 23608*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmbr2 23607 presupposes that 𝐹 is a function. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢))))
Theorem	lmconst 23609	A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝑃})(⇝𝑡‘𝐽)𝑃)
Theorem	lmcvg 23610*	Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑈)
Theorem	iscnp4 23611*	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 23612*	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 23613	An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.)
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽)
Theorem	cnco 23614	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 23615	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 23616	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 23617*	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 23618	Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐽)‘(◡𝐹 “ 𝑆)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑆)))
Theorem	cnntri 23619	Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → (◡𝐹 “ ((int‘𝐾)‘𝑆)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑆)))
Theorem	cnclsi 23620	Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)))
Theorem	cncls2 23621*	Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑌((cls‘𝐽)‘(◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑥)))))
Theorem	cncls 23622*	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 23623*	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 23624	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 23625	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 23626	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 23627	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 23628*	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 23629*	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 23630*	Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑝 ∈ 𝑋 ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑝)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑝})(𝐹 “ 𝑣) ⊆ 𝑤))
Theorem	cnconst2 23631	A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ 𝑌) → (𝑋 × {𝐵}) ∈ (𝐽 Cn 𝐾))
Theorem	cnconst 23632	A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐵 ∈ 𝑌 ∧ 𝐹:𝑋⟶{𝐵})) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	cnrest 23633	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 23634	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 23635	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 23636	One direction of cnprest 23637 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 23637	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 23638	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 23639	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 23640	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 23641	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 23642	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 23643	If 𝐹 converges, then 𝐹 is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ∈ (𝑋 ↑pm ℂ))
Theorem	lmfss 23644	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 23645	Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝑃 ∈ 𝑋)
Theorem	lmss 23646	Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ 𝐾 = (𝐽 ↾t 𝑌)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑌)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹(⇝𝑡‘𝐾)𝑃))
Theorem	sslm 23647	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 23648	A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ↾ (ℤ≥‘𝑀))(⇝𝑡‘𝐽)𝑃))
Theorem	lmff 23649*	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 23650*	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 23651*	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 23652	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 23653	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 𝐾))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃))
12.1.10  Separated spaces: T0, T1, T2 (Hausdorff) ...
Syntax	ct0 23654	Extend class notation with the class of all T0 spaces.
class Kol2
Syntax	ct1 23655	Extend class notation to include T1 spaces (also called Fréchet spaces).
class Fre
Syntax	cha 23656	Extend class notation with the class of all Hausdorff spaces.
class Haus
Syntax	creg 23657	Extend class notation with the class of all regular topologies.
class Reg
Syntax	cnrm 23658	Extend class notation with the class of all normal topologies.
class Nrm
Syntax	ccnrm 23659	Extend class notation with the class of all completely normal topologies.
class CNrm
Syntax	cpnrm 23660	Extend class notation with the class of all perfectly normal topologies.
class PNrm
Definition	df-t0 23661*	Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2735): 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 23695) 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 23662*	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 23663*	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 23664*	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 23665*	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 23666*	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 23667*	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 23668*	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 23693. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)))
Theorem	ist1 23669*	The predicate "is a T1 space". (Contributed by FL, 18-Jun-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Fre ↔ (𝐽 ∈ Top ∧ ∀𝑎 ∈ 𝑋 {𝑎} ∈ (Clsd‘𝐽)))
Theorem	ishaus 23670*	The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
Theorem	iscnrm 23671*	The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ CNrm ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm))
Theorem	t0sep 23672*	Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥) → 𝐴 = 𝐵))
Theorem	t0dist 23673*	Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Kol2 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 ¬ (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜))
Theorem	t1sncld 23674	In a T1 space, singletons are closed. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋) → {𝐴} ∈ (Clsd‘𝐽))
Theorem	t1ficld 23675	In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ (Clsd‘𝐽))
Theorem	hausnei 23676*	Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑃 ≠ 𝑄)) → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ 𝑄 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))
Theorem	t0top 23677	A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Kol2 → 𝐽 ∈ Top)
Theorem	t1top 23678	A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Top)
Theorem	haustop 23679	A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.)
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)
Theorem	isreg 23680*	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 23681	A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Reg → 𝐽 ∈ Top)
Theorem	regsep 23682*	In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Reg ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ ((cls‘𝐽)‘𝑥) ⊆ 𝑈))
Theorem	isnrm 23683*	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 23684	A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top)
Theorem	cnrmtop 23685	A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Top)
Theorem	iscnrm2 23686*	The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ CNrm ↔ ∀𝑥 ∈ 𝒫 𝑋(𝐽 ↾t 𝑥) ∈ Nrm))
Theorem	ispnrm 23687*	The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ PNrm ↔ (𝐽 ∈ Nrm ∧ (Clsd‘𝐽) ⊆ ran (𝑓 ∈ (𝐽 ↑m ℕ) ↦ ∩ ran 𝑓)))
Theorem	pnrmnrm 23688	A perfectly normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Nrm)
Theorem	pnrmtop 23689	A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ PNrm → 𝐽 ∈ Top)
Theorem	pnrmcld 23690*	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 23691*	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 23692*	The predicate "is a T0 space". (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)))
Theorem	ist0-3 23693*	The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑜 ∈ 𝐽 ((𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜) ∨ (¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜)))))
Theorem	cnt0 23694	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 23695*	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 23696	A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Kol2)
Theorem	ist1-3 23697*	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 23698	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 23699*	Express the predicate "𝐽 is a Hausdorff space." (Contributed by NM, 8-Mar-2007.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
Theorem	haust1 23700	A Hausdorff space is a T1 space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Fre)