extend

Mathlib.CategoryTheory.Limits.Cones

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cocones.extend

Lean4

/-- There is a morphism from a cocone to its extension. -/
@[simps]
def extend (s : Cocone F) {X : C} (f : s.pt ⟶ X) : s ⟶ s.extend f where hom := f

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

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

Разделы

Аффилиация

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