coe_disjoint — Mathlib

English

For lists l1, l2, disjointness of their multiset representations is equivalent to list disjointness: Disjoint ((l1) : Multiset) l2 ↔ l1.Disjoint l2.

Русский

Для списков l1, l2: непересечение их отображений в мультисеты эквивалентно некотрому свойству списка: Disjoint((l1 : Multiset)) l2 ↔ l1.Disjoint l2.

LaTeX

$$$ \\mathrm{Disjoint}((l_1 : Multiset\\,\\alpha), l_2) \\iff l_1 \\,\\text{Disjoint}\\, l_2 $$$

Lean4

@[simp, norm_cast]
theorem coe_disjoint (l₁ l₂ : List α) : Disjoint (l₁ : Multiset α) l₂ ↔ l₁.Disjoint l₂ :=
  disjoint_left

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