coe_symm_toEquiv

Mathlib.RingTheory.Coalgebra.Equiv

URI: https://scilib.ai/kg/mathlib#CoalgEquiv.coe_symm_toEquiv

English

For a coalgebra equivalence e, the function underlying e.toEquiv.symm coincides with e.symm.

Русский

Для коалгебраической эквивалентности e функция, лежащая в основе e.toEquiv.symm, совпадает с e.symm.

LaTeX

$$$ \\forall x, \\; \\big( e.toEquiv \\big)^{-1}(x) = e^{-1}(x) $$$

Lean4

@[simp]
theorem coe_symm_toEquiv : ⇑e.toEquiv.symm = e.symm :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru