toEquiv_fun

Mathlib.CategoryTheory.Types.Basic

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

English

For i: X ≅ Y, the underlying function of i.toEquiv is exactly i.hom; i.e., (i.toEquiv : X → Y) = i.hom.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toEquiv_fun (i : X ≅ Y) : (i.toEquiv : X → Y) = i.hom :=
  rfl

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

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

Разделы

Аффилиация

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