nonempty_Ioo — Mathlib

English

If α is densely ordered, then the open interval Ioo a b is nonempty exactly when a < b.

Русский

Если порядок плотно упорядочен, то открытый интервал Ioo a b непуст тогда и только тогда, когда a < b.

LaTeX

$$$$ [DenselyOrdered \\alpha] \\Rightarrow (\\mathrm{Ioo}\\ a\\ b).\\mathrm{Nonempty} \\iff a < b. $$$$

Lean4

@[simp]
theorem nonempty_Ioo [DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b :=
  ⟨fun ⟨_, ha, hb⟩ => ha.trans hb, exists_between⟩

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