nhds_one_symm' — Mathlib

English

The image of the neighborhood of 1 under inversion equals the neighborhood of 1: map inv (nhds 1) = nhds 1.

Русский

Образ окрестности единицы под инверсией равен окрестности единицы: map inv (nhds 1) = nhds 1.

LaTeX

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

Lean4

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

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