limitRecOn_pred_of_not_isMin — Mathlib

English

If hb is Not IsMin b, then the limitRecOn at (Order.pred b) equals pred b hb (limitRecOn b pred isPredLimit).

Русский

Если hb: Not IsMin(b), то limitRecOn на Order.pred b равен pred b hb (limitRecOn b pred isPredLimit).

LaTeX

$$$\\text{limitRecOn}(\\mathrm{Order.pred}(b)) = \\mathrm{pred}(b)(hb)(\\text{limitRecOn}(b, pred, isPredLimit))$$$

Lean4

theorem limitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    limitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb (limitRecOn b isMax pred isPredLimit) :=
  SuccOrder.limitRecOn_succ_of_not_isMax (α := αᵒᵈ) isMax pred _ hb

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