le_pushouts

Mathlib.CategoryTheory.MorphismProperty.Limits

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

English

For any p, if P(p) then P.pushouts(p).

Русский

Для любого p, если P(p), то P.pushouts(p).

LaTeX

$$P(p) \Rightarrow P.pushouts(p)$$

Lean4

theorem le_pushouts : P ≤ P.pushouts := by
  intro X Y p hp
  exact P.pushouts_mk IsPushout.of_id_fst hp

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

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

Разделы

Аффилиация

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