English
If X is a T25Space, then the subtype {x ∈ X | p x} has T25Space.
Русский
Если X — T25-пространство, то подпроизвид {x ∈ X | p x} имеет T25Space.
LaTeX
$$$[T25Space X] \Rightarrow [T25Space (Subtype p)].$$$
Lean4
/-- Given two points `x ≠ y`, we can find neighbourhoods `x ∈ V₁ ⊆ U₁` and `y ∈ V₂ ⊆ U₂`,
with the `Vₖ` closed and the `Uₖ` open, such that the `Uₖ` are disjoint. -/
theorem disjoint_nested_nhds [T3Space X] {x y : X} (h : x ≠ y) :
∃ U₁ ∈ 𝓝 x,
∃ V₁ ∈ 𝓝 x,
∃ U₂ ∈ 𝓝 y,
∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂ :=
by
rcases t2_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩
rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩
rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩
exact
⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in, V₁_closed, V₂_closed, U₁_op,
U₂_op, h₁, h₂, H⟩
