Ioc_disjoint_Ioc — Mathlib

English

Disjointness of two Ioc intervals is equivalent to min endpoints ≤ max opposite endpoints: Disjoint(Ioc(a1,a2), Ioc(b1,b2)) ↔ min(a2,b2) ≤ max(a1,b1).

Русский

Непересечение интервалов Ioc(a1,a2) и Ioc(b1,b2) эквивалентно сравнению концов: min(a2,b2) ≤ max(a1,b1).

LaTeX

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

Lean4

@[simp]
theorem Ioc_disjoint_Ioc : Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ :=
  by
  have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
  simpa only [Ico_toDual] using h

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