isSuccLimitRecOn_succ_of_not_isMax

English

If b is not a maximum, then the succ-based limit recursion at succ(b) equals succ(b) with hb.

Русский

Если b не максимум, предел-рекурсия на succ(b) равна succ(b, hb).

LaTeX

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

Lean4

theorem isSuccLimitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
    isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb := by
  rw [isSuccLimitRecOn, isSuccPrelimitRecOn_succ_of_not_isMax]

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