count_eq_card_filter_eq — Mathlib

English

For a decidable equality, the count of a in s equals the cardinality of the set of occurrences of a in s, i.e., the filter by a.

Русский

При детерминированном равенстве счёт элемента a в s равен мощности множества его вхождений, то есть фильтр по a.

LaTeX

$$$ s.count\\,a = \\mathrm{card}(s.filter (a = \\cdot)) $$$

Lean4

theorem count_eq_card_filter_eq [DecidableEq α] (s : Multiset α) (a : α) : s.count a = card (s.filter (a = ·)) := by
  rw [count, countP_eq_card_filter]

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