strictColimitsOfShape_le_colimitsOfShape

English

For all X, a strict shape colimit implies the ordinary shape colimit: P.strictColimitsOfShape J ≤ P.colimitsOfShape J.

Русский

Для всех X строгий колимит по форме J включает обычный колимит по форме J: P.strictColimitsOfShape J ≤ P.colimitsOfShape J.

LaTeX

$$$$ P.strictColimitsOfShape(J) \le P.colimitsOfShape(J). $$$$

Lean4

theorem strictColimitsOfShape_le_colimitsOfShape : P.strictColimitsOfShape J ≤ P.colimitsOfShape J :=
  by
  rintro X ⟨F, hF⟩
  exact ⟨.colimit F hF⟩

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