obj_limit — Mathlib

English

The isColimit for coconeOfLE iter.F hij identifies with the colimit of the restriction LT.

Русский

IsColimit для кокона coconeOfLE iter.F hij совпадает с колимитом ограничения LT.

LaTeX

$$$ \\text{isColimit}(coconeOfLE iter.F hij) = \\text{colimit}(restrictionLT iter.F hij) $$$

Lean4

theorem obj_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) :
    letI := hasColimitsOfShape_of_isSuccLimit C i hi
    iter.F.obj ⟨i, hij⟩ = colimit (restrictionLT iter.F hij) :=
  congr_arg Comma.right (iter.arrowMap_limit i hi hij ⊥ (Order.IsSuccLimit.bot_lt hi))

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