isPredLimitRecOn_pred — Mathlib

English

Final form of pred recursion at non-min elements.

Русский

Финальная форма рекурсии по pred для не минимальных элементов.

LaTeX

$$$\\mathrm{isPredLimitRecOn}(\\mathrm{Order.pred}(b), isMax, pred, isPredLimit) = pred(b, not\\_isMin(b)).$$$

Lean4

@[simp]
theorem isPredLimitRecOn_pred [NoMinOrder α] :
    isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b (not_isMin b) :=
  isSuccLimitRecOn_succ (α := αᵒᵈ) isMax pred _ b

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