isPredLimitRecOn_of_isPredLimit — Mathlib

English

Simplicity form of the pred recursion at not-minimal case.

Русский

Упрощенная форма пред-рекурсии при не минимальном случае.

LaTeX

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

Lean4

@[simp]
theorem isPredLimitRecOn_of_isPredLimit (hb : IsPredLimit b) :
    isPredLimitRecOn b isMax pred isPredLimit = isPredLimit b hb :=
  isSuccLimitRecOn_of_isSuccLimit (α := αᵒᵈ) isMax pred _ hb.dual

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