ndunion_eq — Mathlib

English

If s and t are disjoint, then s.ndunion t equals s.dedup + t.

Русский

Если s и t несовместны, то s.ndunion t = s.dedup + t.

LaTeX

$$$\\text{Disjoint}(s,t) \\Rightarrow \\mathrm{ndunion}(s,t) = s \\mathrm{+} t^{\\;red}$$$

Lean4

theorem ndunion_eq {s t : Multiset α} (h : Disjoint s t) : s.ndunion t = s.dedup + t :=
  by
  induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.union_eq <| by simpa using h

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