toEquiv_symm — Mathlib

English

Let f be an ordered monoid isomorphism between α and β. Then the underlying equivalence of its inverse equals the inverse of the underlying equivalence: f.symm.toEquiv = (f.toEquiv).symm.

Русский

Пусть f — упорядоченная изоморфизм-многочлен между α и β. Тогда соответствие обратного отображения равно обратному соответствию исходного отображения: f.symm.toEquiv = (f.toEquiv).symm.

LaTeX

$$$(f^{-1})_{eq} = (f_{eq})^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem toEquiv_symm (f : α ≃*o β) : (f.symm : β ≃ α) = (f : α ≃ β).symm :=
  rfl

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