coe_toEquiv_symm — Mathlib

English

The underlying function of the inverse coalgebra equivalence’s underlying equivalence matches the inverse of the underlying equivalence.

Русский

Функция, лежащая в основе обратной эквивалентности коалгебр, совпадает с обратной функцией базовой эквивалентности.

LaTeX

$$$e.toEquiv.symm = e.symm$$$

Lean4

theorem coe_toEquiv_symm : e.toEquiv.symm = e.symm :=
  rfl

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