colimitsOfShape_discrete_le_llp_rlp

English

For any shape J, the colimits of shape Discrete J are contained in LLP of RLP: T.colimitsOfShape(Discrete J) ≤ T.rlp.llp.

Русский

Для любой формы J копмпоненты котраной Discrete J содержатся в LLP от RLP: T.colimitsOfShape(Discrete J) ≤ T.rlp.llp.

LaTeX

$$$T.colimitsOfShape(Discrete J) \le T.rlp.llp$$$

Lean4

theorem colimitsOfShape_discrete_le_llp_rlp (J : Type w) : T.colimitsOfShape (Discrete J) ≤ T.rlp.llp :=
  by
  intro A B i hi
  exact MorphismProperty.colimitsOfShape_le _ (colimitsOfShape_monotone T.le_llp_rlp _ _ hi)

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