count_union — Mathlib

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]

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