toIsometryEquiv_symm — Mathlib

English

If e is a linear isometry equivalence, then the isometry part of its inverse equals the inverse of its isometry part.

Русский

Если e — линейное изометрическое эквивалентное отображение, то изометрическая часть его обратного равна обратному изометру.

LaTeX

$$$ e^{\\mathrm{symm}}_{Isom} = (e^{Isom})^{-1} $$$

Lean4

@[simp]
theorem toIsometryEquiv_symm : e.symm.toIsometryEquiv = e.toIsometryEquiv.symm :=
  rfl

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