app_hom

Mathlib.CategoryTheory.Abelian.Pseudoelements

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.app_hom

Lean4

@[simp]
theorem app_hom {P Q : C} (f : P ⟶ Q) (a : Over P) : (app f a).hom = a.hom ≫ f :=
  rfl

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

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

Разделы

Аффилиация

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