nhds_coe_units — Mathlib

English

The neighborhood filter at a unit γ equals the pure γ as a filter on Γ₀.

Русский

Окрестности единицы γ равны чистой массой γ в Γ₀.

LaTeX

$$$\mathcal{N}(γ) = \mathrm{pure}(γ) \quad (γ \in Γ₀^×)$$$

Lean4

/-- The neighbourhood filter of an invertible element consists of all sets containing that
element. -/
theorem nhds_coe_units (γ : Γ₀ˣ) : 𝓝 (γ : Γ₀) = pure (γ : Γ₀) :=
  nhds_of_ne_zero γ.ne_zero

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