nhds_one_symm — Mathlib

English

The inverse image under the inversion map of the neighborhood at 1 is the neighborhood at 1 itself; i.e., comap inv at nhds 1 equals nhds 1.

Русский

Обратный образ под отображением инверсии окрестности в точке 1 совпадает с окрестностью в точке 1.

LaTeX

$$$\mathrm{comap}\,\mathrm{Inv.inv} (\mathcal{N}(1_G)) = \mathcal{N}(1_G)$$$

Lean4

@[to_additive]
theorem nhds_one_symm : comap Inv.inv (𝓝 (1 : G)) = 𝓝 (1 : G) :=
  ((Homeomorph.inv G).comap_nhds_eq _).trans (congr_arg nhds inv_one)

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