Ioi_sub_one_eq_Ici

Mathlib.Algebra.Order.Interval.Set.SuccPred

URI: https://scilib.ai/kg/mathlib#Set.Ioi_sub_one_eq_Ici

English

For any a with NoMinOrder, Ioi(a−1) = Ici(a).

Русский

Для любого a с NoMinOrder выполняется Ioi(a−1) = Ici(a).

LaTeX

$$$ Ioi(a - 1) = Ici(a) $$$

Lean4

theorem Ioi_sub_one_eq_Ici (a : α) : Ioi (a - 1) = Ici a := by simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru