inv_eqToHom

Mathlib.CategoryTheory.EqToHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.inv_eqToHom

English

The inverse of eqToHom h is eqToHom h.symm.

Русский

Обратный к eqToHom h равен eqToHom h.symm.

LaTeX

$$$ \\operatorname{inv}(\\mathrm{eqToHom}(h)) = \\mathrm{eqToHom}(h^{\\mathrm{symm}}) $$$

Lean4

@[simp]
theorem inv_eqToHom {X Y : C} (h : X = Y) : inv (eqToHom h) = eqToHom h.symm := by cat_disch

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

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

Разделы

Аффилиация

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