toEquiv_symm_fun

Mathlib.CategoryTheory.Types.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.toEquiv_symm_fun

English

For i: X ≅ Y, the function underlying i.toEquiv.symm is i.inv; i.e., (i.toEquiv.symm : Y → X) = i.inv.

Русский

Пусть i: X ≅ Y; функция, лежащая в основе i.toEquiv.symm, равна i.inv; то есть (i.toEquiv.symm : Y → X) = i.inv.

LaTeX

$$$ (i.toEquiv.symm : Y \\to X) = i.inv $$$

Lean4

@[simp]
theorem toEquiv_symm_fun (i : X ≅ Y) : (i.toEquiv.symm : Y → X) = i.inv :=
  rfl

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

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

Разделы

Аффилиация

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