isPredPrelimitRecOn_pred_of_not_isMin

English

If b is not minimal, the predecessor recursion at pred(b) yields pred(b) with hb not minimal.

Русский

Если b не минимален, рекурсия по предшественнику на pred(b) даёт pred(b) с hb non-minimal.

LaTeX

$$$\\mathrm{isPredPrelimitRecOn}(\\mathrm{Order.pred}(b))=\\mathrm{pred}(b, hb)$, with $hb: \\neg IsMin(b)$.$$

Lean4

theorem isPredPrelimitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb :=
  isSuccPrelimitRecOn_succ_of_not_isMax (α := αᵒᵈ) _ _ _

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