singleton_mem_nhds_of_ne_zero — Mathlib

English

For a nonzero γ, the singleton {γ} is a neighborhood of γ.

Русский

Для не нулевого γ множество {γ} является окрестностью γ.

LaTeX

$$$\\{γ\\} \in \\mathcal{N}(γ)$$$

Lean4

/-- If `γ` is a nonzero element of a linearly ordered group with zero element adjoined, then `{γ}`
is a neighbourhood of `γ`. -/
theorem singleton_mem_nhds_of_ne_zero (h : γ ≠ 0) : ({ γ } : Set Γ₀) ∈ 𝓝 (γ : Γ₀) := by simp [h]

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