count_inter — Mathlib

English

For any a, count a in s ∩ t equals min(count a s, count a t).

Русский

Для любого элемента a количество a в s ∩ t равно min(count a s, count a t).

LaTeX

$$$ \\operatorname{count}(a, s \\cap t) = \\min\\big( \\operatorname{count}(a, s), \\operatorname{count}(a, t) \\big) $$$

Lean4

@[simp]
theorem count_inter (a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t) :=
  by
  apply @Nat.add_left_cancel (count a (s - t))
  rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]

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