pushouts_monotone

Mathlib.CategoryTheory.MorphismProperty.Limits

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

English

If P ≤ Q then P.pushouts ≤ Q.pushouts.

Русский

Если P ≤ Q, то P.pushouts ≤ Q.pushouts.

LaTeX

$$P \le Q \Rightarrow P.pushouts \le Q.pushouts$$

Lean4

theorem pushouts_monotone : Monotone (pushouts (C := C)) :=
  by
  rintro _ _ h _ _ _ ⟨_, _, _, _, _, hp, sq⟩
  exact ⟨_, _, _, _, _, h _ hp, sq⟩

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

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

Разделы

Аффилиация

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