Ioi_sub_one_eq_Ici_of_not_isMin

Mathlib.Algebra.Order.Interval.Set.SuccPred

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

English

If a is not minimal, then Ioi(a−1) = Ici(a).

Русский

Если a не минимален, то Ioi(a−1) = Ici(a).

LaTeX

$$$ \neg \mathrm{IsMin}(a) \implies \mathrm{Ioi}(a - 1) = \mathrm{Ici}(a) $$$

Lean4

theorem Ioi_sub_one_eq_Ici_of_not_isMin (ha : ¬IsMin a) : Ioi (a - 1) = Ici a := by
  simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici_of_not_isMin ha

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

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

Разделы

Аффилиация

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