toIso_hom

Mathlib.CategoryTheory.Types.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.toIso_hom

English

For any equivalence e: X ≃ Y, the hom component of toIso(e) equals e itself as a function: toIso(e).hom = e.

Русский

Для эквивалентности e: X ≃ Y компоненту hom у toIso(e) соответствует сама функция e: toIso(e).hom = e.

LaTeX

$$$$ \mathrm{toIso}(e).\mathrm{hom} = e. $$$$

Lean4

@[simp]
theorem toIso_hom {e : X ≃ Y} : e.toIso.hom = e :=
  rfl

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

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

Разделы

Аффилиация

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