isSuccLimitRecOn_succ — Mathlib

English

Under NoMaxOrder, the simp version holds for the succ case.

Русский

При NoMaxOrder справедливо упрощенное утверждение для случая succ.

LaTeX

$$$\\mathrm{isSuccLimitRecOn\\_succ}[NoMaxOrder](b) : \\mathrm{isSuccLimitRecOn}(\\mathrm{Order.succ}(b), \\dots) = \\mathrm{succ}(b, \\neg IsMax(b)).$$$

Lean4

@[simp]
theorem isSuccLimitRecOn_succ [NoMaxOrder α] (b : α) :
    isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b (not_isMax b) :=
  isSuccLimitRecOn_succ_of_not_isMax isMin succ isSuccLimit _

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