Ioc_disjoint_Ioc — Mathlib

English

Two open intervals Ioc(a1,a2) and Ioc(b1,b2) are disjoint if and only if min(a2,b2) ≤ max(a1,b1).

Русский

Два открытых интервала Ioc(a1,a2) и Ioc(b1,b2) несовместны тогда и только тогда, когда min(a2,b2) ≤ max(a1,b1).

LaTeX

$$Disjoint(Ioc(a1,a2), Ioc(b1,b2)) \iff \min(a2,b2) \le \max(a1,b1)$$

Lean4

@[simp]
theorem Ioc_disjoint_Ioc : Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
  simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]

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