English
Let α be a linear order with a successor operation and no maximum element. Then the open interval Ioo(a, b) is empty if and only if b is at most the successor of a, i.e. b ≤ succ(a).
Русский
Пусть α — линейный порядок с операцией следующего элемента и без максимального элемента. Тогда открытый интервал Ioo(a, b) пуст тогда и только тогда, когда b не больше succ(a), то есть b ≤ succ(a).
LaTeX
$$$ Ioo(a,b) = \emptyset \iff b \le \operatorname{succ}(a) $$$
Lean4
@[simp]
theorem Ioo_eq_empty_iff_le_succ : Ioo a b = ∅ ↔ b ≤ succ a :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· contrapose! h
exact ⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩
· ext x
suffices a < x → b ≤ x by simpa
exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx
