nhds_inv₀ — Mathlib

English

For x ≠ 0 in a group with zero, the neighborhood filter at x⁻¹ is the image of the neighborhood filter at x under inversion.

Русский

Для x ≠ 0 в группе с нулём топология окружности x⁻¹ равна образу окружности x под операцией инверсии.

LaTeX

$$\\text{nhds}_{G_0}(x^{-1}) = (\\text{nhds}_{G_0}(x))^{-1} \\quad (x \\neq 0)$$

Lean4

theorem nhds_inv₀ (hx : x ≠ 0) : 𝓝 x⁻¹ = (𝓝 x)⁻¹ :=
  by
  refine le_antisymm (inv_le_iff_le_inv.1 ?_) (tendsto_inv₀ hx)
  simpa only [inv_inv] using tendsto_inv₀ (inv_ne_zero hx)

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