obj_succ — Mathlib

English

For iter : Φ.Iteration j, i ≤ j and hi being a succ-limit, the object iter.F.obj ⟨i, hi⟩ is the colimit of restrictionLT iter.F hij.

Русский

Для итерации iter на предельном элементе i с i ≤ j и hi суффиксный предел, объект iter.F.i равен колимиту ограничений restrictionLT iter.F hij.

LaTeX

$$$ \\operatorname{iter}.F.obj ⟨i, hij⟩ = \\operatorname{colimit}(\\restrictionLT iter.F hij) $$$

Lean4

theorem obj_succ (i : J) (hi : i < j) :
    iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = Φ.succ (iter.F.obj ⟨i, hi.le⟩) :=
  congr_arg Comma.right (iter.arrowSucc_eq i hi)

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