coe_toEquiv_symm

Mathlib.Algebra.Order.Hom.Monoid

URI: https://scilib.ai/kg/mathlib#OrderMonoidIso.coe_toEquiv_symm

← MathLib Explorer

English

EquivLike.inv f equals f.symm.

Русский

EquivLike.inv f равно f.symm.

LaTeX

$$equivLike_inv_eq_symm (f : α \simeq^*o β) : EquivLike.inv f = f.symm$$

Lean4

/-- `simp`-normal form of `invFun_eq_symm`. -/
@[to_additive (attr := simp)]
theorem coe_toEquiv_symm (f : α ≃*o β) : ((f : α ≃ β).symm : β → α) = f.symm :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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