Iio_add_one_eq_Iic — Mathlib

English

Let α be a linear ordered set with 1, addition, and SuccAddOrder, and assume there is no maximum element. Then for every b ∈ α, Iio(b+1) = Iic(b).

Русский

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

LaTeX

$$$ Iio(b+1) = Iic(b) $$$

Lean4

theorem Iio_add_one_eq_Iic (b : α) : Iio (b + 1) = Iic b := by simpa [succ_eq_add_one] using Iio_succ_eq_Iic b

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