prelimitRecOn_pred_of_not_isMin — Mathlib

English

If b is not minimal, then the value of prelimitRecOn at Order.pred b is equal to pred b hb (prelimitRecOn b pred isPredPrelimit).

Русский

Если b не минимален, тогда значение prelimitRecOn на Order.pred b равно pred b hb (prelimitRecOn b pred isPredPrelimit).

LaTeX

$$$\\text{hb} : \\neg \\mathrm{IsMin}(b) \\Rightarrow \\mathrm{prelimitRecOn}(\\mathrm{Order.pred}(b)) = \\mathrm{pred}(b, \\mathrm{hb})(\\mathrm{prelimitRecOn}(b, pred, isPredPrelimit))$$$

Lean4

theorem prelimitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb (prelimitRecOn b pred isPredPrelimit) :=
  SuccOrder.prelimitRecOn_succ_of_not_isMax _ _ _

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