eqToHom_right

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Under.eqToHom_right

Lean4

@[simp]
theorem eqToHom_right {X : T} {U V : Under X} (e : U = V) : (eqToHom e).right = eqToHom (e ▸ rfl : U.right = V.right) :=
  by subst e; rfl

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

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

Разделы

Аффилиация

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