Iio_add_one_eq_Iic_of_not_isMax — Mathlib

English

Let α be a linear ordered set with a successor operation, and let b be an element that is not maximal. Then the open-interval to the left of b+1 equals the closed-interval to the left of b: Iio(b+1) = Iic(b).

Русский

Пусть α — линеаризованное множество с операцией перехода к следующему элементу, и пусть b не является максимальным. Тогда открытый интервал слева от b+1 совпадает с закрытым интервалом слева от b: Iio(b+1) = Iic(b).

LaTeX

$$$ \neg \mathrm{IsMax}(b) \implies \mathrm{Iio}(b+1) = \mathrm{Iic}(b) $$$

Lean4

theorem Iio_add_one_eq_Iic_of_not_isMax (hb : ¬IsMax b) : Iio (b + 1) = Iic b := by
  simpa [succ_eq_add_one] using Iio_succ_eq_Iic_of_not_isMax hb

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