Ico_succ_right_of_not_isMax — Mathlib

English

Let α be a linear order with a successor operation. If b is not a maximal element, then the half-open interval from a to succ(b) coincides with the closed interval from a to b; i.e. Ico(a, succ(b)) = Icc(a, b).

Русский

Пусть α — линейный порядок с операцией следующего элемента. Если b не максимален, то полупреступная интервалная часть от a до succ(b) совпадает с замкнутым интервалом от a до b; то есть Ico(a, succ(b)) = Icc(a, b).

LaTeX

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

Lean4

theorem Ico_succ_right_of_not_isMax (hb : ¬IsMax b) : Ico a (succ b) = Icc a b := by
  rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]

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