nhds_inter_eq_singleton_of_mem_discrete

English

Let s be a discrete subset and x ∈ s. There exists an open set U with U ∈ 𝓝 x and U ∩ s = {x}.

Русский

Пусть s — дискретное подмножество и x ∈ s. Тогда существует открытое множество U такое, что U ∈ 𝓝 x и U ∩ s = {x}.

LaTeX

$$$ \\forall X [TopologicalSpace X] {s} [DiscreteTopology s] {x} (hx:s ∈ x), \\exists U \\in 𝓝 x, U \\cap s = {x}. $$$

Lean4

/-- A point `x` in a discrete subset `s` of a topological space admits a neighbourhood
that only meets `s` at `x`. -/
theorem nhds_inter_eq_singleton_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X} (hx : x ∈ s) :
    ∃ U ∈ 𝓝 x, U ∩ s = { x } := by simpa using (𝓝 x).basis_sets.exists_inter_eq_singleton_of_mem_discrete hx

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