limitRecOn_of_isSuccLimit — Mathlib

English

Limit recursion on succ reduces to succ applied to b with not_isMax witness, recursively.

Русский

Предел-рекурсия на succ сводится к применению succ к b с witness not_isMax и рекурсивно.

LaTeX

$$$\\mathrm{limitRecOn}(\\mathrm{Order.succ}(b)) = \\mathrm{succ}(b, \\lnot IsMax(b)) (\\mathrm{limitRecOn}(b)).$$$

Lean4

@[simp]
theorem limitRecOn_of_isSuccLimit (hb : IsSuccLimit b) :
    limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun x _ ↦ limitRecOn x isMin succ isSuccLimit := by
  rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_neg hb.not_isMin]; rfl

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