nhds_of_ne_zero — Mathlib

English

If γ ≠ 0, the neighborhood filter at γ is the pure γ (point mass at γ).

Русский

Если γ ≠ 0, окрестности γ равны чистой массой на γ.

LaTeX

$$$\mathcal{N}(γ) = \mathrm{pure}(γ)\quad (γ \neq 0)$$$

Lean4

/-- The neighbourhood filter of a nonzero element consists of all sets containing that
element. -/
@[simp]
theorem nhds_of_ne_zero {γ : Γ₀} (h₀ : γ ≠ 0) : 𝓝 γ = pure γ :=
  nhds_nhdsAdjoint_of_ne _ h₀

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