limitRecOn_succ_of_not_isMax — Mathlib

English

Alias relation of limit recursion at succ for not-max case.

Русский

Алиас-отношение предел-рекурсии на succ для не максимального элемента.

LaTeX

$$$\\mathrm{limitRecOn}(\\mathrm{Order.succ}(b)) = \\mathrm{succ}(b, hb) (\\mathrm{limitRecOn}(b))$ with $hb: \\neg IsMax(b)$.$$

Lean4

theorem limitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
    limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (limitRecOn b isMin succ isSuccLimit) := by
  rw [limitRecOn, prelimitRecOn_succ_of_not_isMax]; rfl

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