Ico_disjoint_Ico — Mathlib

English

For half-open intervals Ico with endpoints a1<a2 and b1<b2 in a linear order, the two sets are disjoint iff min(a2,b2) ≤ max(a1,b1).

Русский

Для полуоткрытых интервалов Ico(a1,a2) и Ico(b1,b2) в линейном порядке непересечение эквивалентно некоему сравнению концевых точек: min(a2,b2) ≤ max(a1,b1).

LaTeX

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

Lean4

@[simp]
theorem Ico_disjoint_Ico : Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
  simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]

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