colimitsOfShape_monotone

Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.colimitsOfShape_monotone

← MathLib Explorer

English

If P ≤ Q, then P.colimitsOfShape J ≤ Q.colimitsOfShape J.

Русский

Если P ≤ Q, то P.colimitsOfShape J ≤ Q.colimitsOfShape J.

LaTeX

$$$$ P \le Q \Rightarrow P.colimitsOfShape(J) \le Q.colimitsOfShape(J). $$$$

Lean4

theorem colimitsOfShape_monotone {Q : ObjectProperty C} (hPQ : P ≤ Q) : P.colimitsOfShape J ≤ Q.colimitsOfShape J :=
  by
  intro X ⟨h⟩
  exact ⟨h.ofLE hPQ⟩

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

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

Разделы

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

Аффилиация

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