English
The multiplicity of a in the union equals the maximum of its multiplicities in the summands: count(a, s ∪ t) = max(count(a, s), count(a, t)).
Русский
Число вхождений a в объединение равно максимуму его вхождений в с и в t: count(a, s ∪ t) = max(count(a, s), count(a, t)).
LaTeX
$$$\\operatorname{count}(a, s \\cup t) = \\max(\\operatorname{count}(a, s), \\operatorname{count}(a, t)).$$$
Lean4
@[simp]
theorem count_union (a : α) (s t : Multiset α) : count a (s ∪ t) = max (count a s) (count a t) := by
simp [(· ∪ ·), union, Nat.sub_add_eq_max]