prelimitRecOn_pred — Mathlib

English

In the pred-order setting, the prelimitRecOn at the predecessor of b equals pred applied to b with the same recursive input.

Русский

В рамках порядка предшественников, prelimitRecOn на предшественнике b равен применению pred к b с тем же рекурсивным входом.

LaTeX

$$$\\mathrm{prelimitRecOn}(\\mathrm{Order.pred}(b)) = \\mathrm{pred}(b)(\\mathrm{notIsMin}(b))\\big( \\mathrm{prelimitRecOn}(b) \\big)$$$

Lean4

@[simp]
theorem prelimitRecOn_pred [NoMinOrder α] (b : α) :
    prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b (not_isMin b) (prelimitRecOn b pred isPredPrelimit) :=
  prelimitRecOn_pred_of_not_isMin _ _ _

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