count_diff — Mathlib

English

For any a, the count of a in the difference l1 \\ l2 equals the count in l1 minus the count in l2.

Русский

Для любого элемента a подсчёт количества a в разности списков l1 \\ l2 равен разности счётчиков a в l1 и в l2.

LaTeX

$$$\\forall a:\\alpha,\\ \\#_a(l_1\\setminus l_2) = \\#_a(l_1) - \\#_a(l_2)$$$

Lean4

theorem count_diff (a : α) (l₁ : List α) : ∀ l₂, count a (l₁.diff l₂) = count a l₁ - count a l₂
  | [] => rfl
  | b :: l₂ => by
    simp only [diff_cons, count_diff, count_erase, beq_iff_eq, Nat.sub_right_comm, count_cons, Nat.sub_add_eq]

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