Iio_add_one_eq_Iic — Mathlib

English

For every element b in a linear order with suitable finiteness, the set of elements strictly less than b+1 coincides with the set of elements less than or equal to b; i.e. x < b+1 if and only if x ≤ b.

Русский

Для любого элемента b в линейном порядке с подходящей сколькостью верно: множество элементов строго меньше b+1 совпадает с множеством элементов, не превышающих b; то есть x < b+1 тогда и только тогда, когда x ≤ b.

LaTeX

$$$\mathrm{Iio}(b+1) = \mathrm{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

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