limitRecOn_of_isPredLimit — Mathlib

English

If b has the IsPredLimit property, the limitRecOn construction coincides with the given isPredLimit data applied to b and hb, recursively.

Русский

Если b имеет свойство IsPredLimit, то конструкция limitRecOn совпадает с данным isPredLimit на b и hb рекурсивно.

LaTeX

$$$\\text{limitRecOn}(b) = \\text{isPredLimit}(b, hb)\\big(\\lambda a,\\_ \\mapsto \\text{limitRecOn}(a)\\big)$$$

Lean4

@[simp]
theorem limitRecOn_of_isPredLimit (hb : IsPredLimit b) :
    limitRecOn b isMax pred isPredLimit = isPredLimit b hb fun x _ ↦ limitRecOn x isMax pred isPredLimit :=
  SuccOrder.limitRecOn_of_isSuccLimit (α := αᵒᵈ) isMax pred _ hb.dual

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