coe_ndinter — Mathlib

English

The ndinter of the multisets corresponding to lists l1 and l2 coincides with the list intersection l1 ∩ l2, up to the natural embedding of lists into multisets.

Русский

Пересечение ndinter соответствующих multisets списков l1 и l2 совпадает с пересечением списков l1 ∩ l2 (с учётом естественного внедрения списков в мультимножества).

LaTeX

$$$\\mathrm{ndinter}(\\mathrm{ofList}(l_1), \\mathrm{ofList}(l_2)) = \\mathrm{ofList}(l_1 \\cap l_2)$$$

Lean4

@[simp]
theorem coe_ndinter (l₁ l₂ : List α) : @ndinter α _ l₁ l₂ = (l₁ ∩ l₂ : List α) :=
  by
  simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]
  apply Perm.refl

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