Ico_succ_left_of_not_isMax

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.Ico_succ_left_of_not_isMax

English

If a is not maximal, then Ico(succ(a), b) = Ioo(a, b).

Русский

Если a не максимален, то Ico(succ(a), b) = Ioo(a, b).

LaTeX

$$$\\neg \\mathrm{IsMax}(a) \\Rightarrow \\mathrm{Ico}(\\operatorname{succ}(a), b) = \\mathrm{Ioo}(a, b)$$$

Lean4

theorem Ico_succ_left_of_not_isMax (ha : ¬IsMax a) : Ico (succ a) b = Ioo a b := by
  rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]

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

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

Разделы

Аффилиация

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