isSuccPrelimitRecOn_succ — Mathlib

English

Under the NoMaxOrder assumption, the prelimit recursion evaluated at the immediate successor equals the successor applied to the predecessor witness.

Русский

При предположении NoMaxOrder рекурсия на предшественнике-усложнении равна переходу к следующему элементу.

LaTeX

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

Lean4

@[simp]
theorem isSuccPrelimitRecOn_succ [NoMaxOrder α] (b : α) :
    isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b (not_isMax b) :=
  isSuccPrelimitRecOn_succ_of_not_isMax _ _ _

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