Ici_succ_eq_Ioi_of_not_isMax

Mathlib.Order.Interval.Set.SuccPred

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

English

If a is not maximal, then Ici(succ a) = Ioi a.

Русский

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

LaTeX

$$$\mathrm{Ici}(\mathrm{succ} a) = \mathrm{Ioi} a$$$

Lean4

theorem Ici_succ_eq_Ioi_of_not_isMax (ha : ¬IsMax a) : Ici (succ a) = Ioi a := by ext x;
  rw [mem_Ici, mem_Ioi, succ_le_iff_of_not_isMax ha]

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

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

Разделы

Аффилиация

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