prelimitRecOn_succ — Mathlib

English

Final dual result tying isPredLimitRecOn to isPredLimit.

Русский

Финальное двойственное утверждение об isPredLimitRecOn и isPredLimit.

LaTeX

$$$\\mathrm{isPredLimitRecOn}(b, isMax, pred, isPredLimit) = \\mathrm{isPredLimit}(b,hb)$ for $hb: IsPredLimit(b).$$$

Lean4

@[simp]
theorem prelimitRecOn_succ [NoMaxOrder α] (b : α) :
    prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b (not_isMax b) (prelimitRecOn b succ isSuccPrelimit) :=
  prelimitRecOn_succ_of_not_isMax _ _ _

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