inv_cobounded₀ — Mathlib

English

The inverse of cobounded α is the nhds-within of zero missing zero: (cobounded α)⁻¹ = 𝓝[≠] 0.

Русский

Обратное к cobounded α равно окружности вокруг нуля без нуля: (cobounded α)⁻¹ = 𝓝[≠] 0.

LaTeX

$$$(\mathrm{cobounded}(\alpha))^{-1} = \mathcal{N}_{\neq 0}.$$$

Lean4

@[simp]
theorem inv_cobounded₀ : (cobounded α)⁻¹ = 𝓝[≠] 0 :=
  by
  rw [← comap_norm_atTop, ← Filter.comap_inv, ← comap_norm_nhdsGT_zero, ← inv_atTop₀, ← Filter.comap_inv]
  simp only [comap_comap, Function.comp_def, norm_inv]

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