succ_pred_iterate_of_not_isMin — Mathlib

English

In a ConditionallyCompleteLattice α with PredOrder α and NoMinOrder α, for all a, pred a equals sSup of Iio a.

Русский

В ConditionallyCompleteLattice α с PredOrder α и NoMinOrder α: pred a = sSup (Iio a).

LaTeX

$$$ \\mathrm{pred}\\ a = \\mathrm{sSup}(\\mathrm{Iio}\\ a) $$$

Lean4

theorem succ_pred_iterate_of_not_isMin (i : α) (n : ℕ) (hin : ¬IsMin (pred^[n - 1] i)) : succ^[n] (pred^[n] i) = i :=
  @pred_succ_iterate_of_not_isMax αᵒᵈ _ _ _ i n hin

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