F₂

Mathlib.CategoryTheory.Limits.Indization.ParallelPair

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NonemptyParallelPairPresentationAux.F₂

English

The cocone Cocone.mk A with ι₁ is a colimit.

Русский

Кокон Cocone.mk A с ι₁ является колимитом.

LaTeX

$$$\text{IsColimit}\big(\mathrm{Cocone.mk}\ A\ (\iota_1\,f\,g\,P_1\,P_2)\big)$$$

Lean4

/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
abbrev F₂ : K f g P₁ P₂ ⥤ C :=
  Comma.snd _ _ ⋙ P₂.F

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

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

Разделы

Аффилиация

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