singleton_mem_nhdsWithin_of_mem_discrete

English

If s is a discrete subset of X and x ∈ s, then {x} lies in the neighborhood filter within s at x, i.e., {x} ∈ 𝓝[s] x.

Русский

Если s — дискретное подмножество X и x ∈ s, то {x} принадлежит фильтру окрестностей внутри s в точке x, то есть {x} ∈ 𝓝[s] x.

LaTeX

$$$ \\forall X [TopologicalSpace X], \\forall s \\subseteq X [DiscreteTopology s], \\forall x \\in s, \\{x\\} \\in 𝓝[s] x.$$$

Lean4

theorem singleton_mem_nhdsWithin_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) :
    { x } ∈ 𝓝[s] x := by
  have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]
  simpa only [nhdsWithin_eq_map_subtype_coe hx, image_singleton] using @image_mem_map _ _ _ ((↑) : s → X) _ this

Похожие утверждения