sum_map_count_dedup_eq_length — Mathlib

English

As a corollary of the previous statement, the sum over dedup elements of their counts equals the length of l: (l.dedup.map (λ x, l.count x)).sum = length l.

Русский

Следствие из предыдущего утверждения: сумма по дедуплицированным элементам их частот равна длине списка: (l.dedup.map (λ x, l.count x)).sum = длина l.

LaTeX

$$(l.dedup.map (\x => l.count x)).sum = l.length$$

Lean4

theorem sum_map_count_dedup_eq_length (l : List α) : (l.dedup.map fun x => l.count x).sum = l.length := by
  simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l

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