Iic_sub_one_eq_Iio — Mathlib

English

For all b, the set of elements not exceeding b−1 equals the set of elements strictly less than b, i.e. Iic(b−1) = Iio(b).

Русский

Для всех b множество элементов, не превышающих b−1, равно множеству элементов, строго меньших чем b.

LaTeX

$$$\mathrm{Iic}(b-1) = \mathrm{Iio}(b)$$$

Lean4

theorem Iic_sub_one_eq_Iio (b : α) : Iic (b - 1) = Iio b := by simpa [pred_eq_sub_one] using Iic_pred_eq_Iio b

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