Ioo_disjoint_Ioo — Mathlib

English

For densely ordered α, two open intervals Ioo(a1,a2) and Ioo(b1,b2) are disjoint iff min(a2,b2) ≤ max(a1,b1).

Русский

В плотно упорядоченном пространстве α два открытых интервала Ioo(a1,a2) и Ioo(b1,b2) непересекаются тогда и только тогда, когда min(a2,b2) ≤ max(a1,b1).

LaTeX

$$$$ \mathrm{Disjoint}(Ioo(a_1,a_2), Ioo(b_1,b_2)) \iff \min(a_2,b_2) \le \max(a_1,b_1) $$$$

Lean4

@[simp]
theorem Ioo_disjoint_Ioo [DenselyOrdered α] : Disjoint (Set.Ioo a₁ a₂) (Set.Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
  simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]

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