coe_inter — Mathlib

English

For lists s, t, the multiset intersection of their ofList representations equals the list bagInter of the lists (viewed as a multiset).

Русский

Для списков s, t пересечение мультимножества, получаемое из их представлений в виде мультимножеств, равно списку bagInter(s, t) (рассматривается как мультимножество).

LaTeX

$$$ (s \\cap t : Multiset \\alpha) = (s . bagInter t : List \\alpha) $$$

Lean4

@[simp]
theorem coe_inter (s t : List α) : (s ∩ t : Multiset α) = (s.bagInter t : List α) := by ext; simp

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