isPredLimitRecOn_pred_of_not_isMin

English

Simplicity variant for pred recursion with not isMin.

Русский

Упрощенный вариант для pred рекурсии при not isMin.

LaTeX

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

Lean4

theorem isPredLimitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb :=
  isSuccLimitRecOn_succ_of_not_isMax (α := αᵒᵈ) isMax pred _ hb

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