hasPushout

Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsPushout.hasPushout

English

If an IsPushout structure exists for f,g,s,t then HasPushout f g exists.

Русский

Если существует структура IsPushout для f,g,s,t, тогда существует HasPushout f g.

LaTeX

$$$ [IsPushout f g] \Rightarrow HasPushout f g $$$

Lean4

theorem hasPushout (h : IsPushout f g inl inr) : HasPushout f g where exists_colimit := ⟨⟨h.cocone, h.isColimit⟩⟩

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

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

Разделы

Аффилиация

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