dedup_add — Mathlib

English

Deduplicating after addition satisfies dedup(s + t) = ndunion s (dedup t).

Русский

После сложения выполняется редукция повторов: dedup(s + t) = ndunion s (dedup t).

LaTeX

$$$\\mathrm{dedup}(s + t) = \\mathrm{ndunion}(s, \\mathrm{dedup}(t))$$$

Lean4

theorem dedup_add (s t : Multiset α) : dedup (s + t) = ndunion s (dedup t) :=
  Quot.induction_on₂ s t fun _ _ => congr_arg ((↑) : List α → Multiset α) <| dedup_append _ _

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