disjoint_coe — Mathlib

English

Two intervals are disjoint iff their underlying sets are disjoint.

Русский

Два интервала являются попарно непересекающимися тогда и только тогда, когда их множества непересекаются.

LaTeX

$$$$ \\text{Disjoint}((s : Set \\alpha), t) \\;\\iff\\; \\text{Disjoint}(s, t). $$$$

Lean4

@[simp, norm_cast]
theorem disjoint_coe (s t : Interval α) : Disjoint (s : Set α) t ↔ Disjoint s t := by
  classical
  rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
  rfl

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