ext_hom_hom

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.BinaryCofan.ext_hom_hom

Lean4

@[simp]
theorem ext_hom_hom {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : c.inl ≫ e.hom = c'.inl)
    (h₂ : c.inr ≫ e.hom = c'.inr) : (ext e h₁ h₂).hom.hom = e.hom :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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