instIsStableUnderCobaseChangePushouts

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangePushouts

← MathLib Explorer

English

Pushouts are stable under cobase change: P.pushouts.IsStableUnderCobaseChange.

Русский

Pushouts устойчивы к каверзному базовому изменению: P.pushouts.IsStableUnderCobaseChange.

LaTeX

$$P.pushouts.IsStableUnderCobaseChange$$

Lean4

instance : P.pushouts.IsStableUnderCobaseChange where
  of_isPushout := by
    rintro _ _ _ _ _ _ _ _ h ⟨_, _, _, _, _, hp, hq⟩
    exact P.pushouts_mk (hq.paste_horiz h) hp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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