toEquiv_symm — Mathlib

English

For any order isomorphism e, the underlying equivalence of e.symm equals the reverse of the underlying equivalence of e.

Русский

Для любой упорядоченной изоморфии e соответствующая ей эквивалентность симметрии e.symm равна обратной эквивалентности e.

LaTeX

$$$ e.symm.toEquiv = e.toEquiv^{-1} $$$

Lean4

@[simp]
theorem toEquiv_symm (e : α ≃o β) : e.symm.toEquiv = e.toEquiv.symm :=
  rfl

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