toIsometryEquiv_symm — Mathlib

English

For any isomorphism i, the corresponding isometry equivalence after applying symmetry equals the symmetry of the associated isometry equivalence.

Русский

Для любой изометрической эквивалентности i симметрия сохраняется через соответствующее преобразование изометрии.

LaTeX

$$$\\text{toIsometryEquiv}(i^{\\mathrm{symm}}) = (\\text{toIsometryEquiv}(i))^{\\mathrm{symm}}$$$

Lean4

@[simp]
theorem toIsometryEquiv_symm (e : X ≅ Y) : toIsometryEquiv e.symm = (toIsometryEquiv e).symm :=
  rfl

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