sum'_app_inl

Mathlib.CategoryTheory.Sums.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.sum'_app_inl

English

For α : F ⟶ G and β : H ⟶ I, the component of sum' on inl a is α.app a.

Русский

Для α : F ⟶ G и β : H ⟶ I компонент sum' на inl a равен α.app a.

LaTeX

$$$ (\\sum' \\alpha \\beta).app (\\mathrm{inl}\\, a) = \\alpha.app a $$$

Lean4

@[simp]
theorem sum'_app_inl {F G : A ⥤ C} {H I : B ⥤ C} (α : F ⟶ G) (β : H ⟶ I) (a : A) : (sum' α β).app (inl a) = α.app a :=
  rfl

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

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

Разделы

Аффилиация

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