limitRecOn_pred — Mathlib

English

In the NoMinOrder context, the pred-order recursion at Order.pred b satisfies the pattern pred b hb (prelimitRecOn b ...).

Русский

В контексте NoMinOrder рекурсия по Order.pred b удовлетворяет схеме pred b hb (prelimitRecOn b ...).

LaTeX

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

Lean4

@[simp]
theorem limitRecOn_pred [NoMinOrder α] (b : α) :
    limitRecOn (Order.pred b) isMax pred isPredLimit = pred b (not_isMin b) (limitRecOn b isMax pred isPredLimit) :=
  SuccOrder.limitRecOn_succ (α := αᵒᵈ) isMax pred _ b

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