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]