count_bagInter — Mathlib

English

The count of a in l1.bagInter l2 equals the minimum of the counts of a in l1 and in l2.

Русский

Количество элемента a в l1.bagInter l2 равно минимуму количеств a в l1 и в l2.

LaTeX

$$$\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] {a : \\\\alpha} {l_1 l_2 : List \\\\alpha},\n count a (l_1.bagInter l_2) = \\min (count a l_1) (count a l_2)$$$

Lean4

@[simp]
theorem count_bagInter {a : α} {l₁ l₂ : List α} : count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂) := by
  fun_induction List.bagInter with grind [count_pos_iff]

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