sub_eq_fold_erase — Mathlib

English

The subtraction of multisets equals folding erase: s - t = foldl erase s t.

Русский

Разность мультимножества равна свертке erase: s - t = foldl erase s t.

LaTeX

$$$s - t = \\mathrm{foldl} \\; \\mathrm{erase} \\; s \\; t$.$$

Lean4

theorem sub_eq_fold_erase (s t : Multiset α) : s - t = foldl erase s t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ =>
    by
    change ofList (l₁.diff l₂) = foldl erase l₁ l₂
    rw [diff_eq_foldl l₁ l₂]
    symm
    exact foldl_hom _ fun x y => rfl

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