isPredPrelimitRecOn_pred — Mathlib

English

Simplified variant of the previous statement under NoMinOrder, giving pred(b) with not_isMin.

Русский

Упрощённый вариант при NoMinOrder: pred(b) с not_isMin.

LaTeX

$$$\\mathrm{isPredPrelimitRecOn}(\\mathrm{Order.pred}(b)) = \\mathrm{pred}(b, \\mathrm{not\\_isMin}(b)).$$$

Lean4

@[simp]
theorem isPredPrelimitRecOn_pred [NoMinOrder α] (b : α) :
    isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b (not_isMin b) :=
  isPredPrelimitRecOn_pred_of_not_isMin _ _ _

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