count_sub — Mathlib

English

For any a ∈ α and multisets s,t, count(a, s − t) = count(a, s) − count(a, t).

Русский

Для любого a ∈ α и мультисетов s,t выполняется count(a, s − t) = count(a, s) − count(a, t).

LaTeX

$$$\operatorname{count}(a, s - t) = \operatorname{count}(a, s) - \operatorname{count}(a, t)$$$

Lean4

@[simp]
theorem count_sub (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t :=
  Quotient.inductionOn₂ s t <| by simp [List.count_diff]

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