nhds_translation_mul_inv₀ — Mathlib

English

For a ≠ 0, comap (· * a⁻¹) (𝓝 1) equals 𝓝 a; i.e., neighborhoods of a correspond to neighborhoods of 1 under the map x ↦ x a⁻¹.

Русский

Для a ≠ 0, сопоставление (comap (x ↦ x a⁻¹)) (𝒩(1)) равно 𝒩(a); т.е. окрестности a соответствуют окрестностям 1 через x a⁻¹.

LaTeX

$$$\\operatorname{comap}(\\cdot * a^{-1})(\\mathcal{N}(1)) = \\mathcal{N}(a)$$$

Lean4

theorem nhds_translation_mul_inv₀ (ha : a ≠ 0) : comap (· * a⁻¹) (𝓝 1) = 𝓝 a :=
  ((Homeomorph.mulRight₀ a ha).symm.comap_nhds_eq 1).trans <| by simp

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