comap_mabs_nhds_one — Mathlib

English

The preimage under the absolute value map of neighborhoods of the identity is exactly the neighborhood of the identity; in particular, comap mabs (nhds 1) = nhds 1.

Русский

Образ обратной предобразности мапы абсолютного значения относительно окрестностей единицы совпадает с окрестностью единицы; в частности, comap mabs (nhds 1) = nhds 1.

LaTeX

$$$\mathrm{comap}\,\mathrm{mabs}\,(\mathcal{N}_1)=\mathcal{N}_1.$$$

Lean4

@[to_additive (attr := simp)]
theorem comap_mabs_nhds_one : comap mabs (𝓝 (1 : G)) = 𝓝 1 := by simp [nhds_eq_iInf_mabs_div]

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