toAutHomeo — Mathlib

English

The underlying map from the equivalence agrees with the underlying map from the basic toAut.

Русский

Базовое отображение из эквивалентности совпадает с отображением из toAut.

LaTeX

$$$toAutMulEquiv\,F\,G\ g = toAut\,F\,G\ g$$$

Lean4

/-- If `G` is a fundamental group for `F`, it is canonically homeomorphic to `Aut F`. -/
noncomputable def toAutHomeo : G ≃ₜ Aut F :=
  (toAut_isHomeomorph F G).homeomorph

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