count_dedup — Mathlib

English

For any l and a, the count of a in dedup(l) equals 1 if a occurs in l, otherwise 0.

Русский

Для любых l и a счёт элемента a в dedup(l) равен 1, если a встречается в l, иначе 0.

LaTeX

$$$\\mathrm{count}(a, \\mathrm{dedup}(l)) = \\begin{cases} 1, & a \\in l \\\\ 0, & a \\notin l \\end{cases}$$$

Lean4

theorem count_dedup (l : List α) (a : α) : l.dedup.count a = if a ∈ l then 1 else 0 := by
  simp_rw [count_eq_of_nodup <| nodup_dedup l, mem_dedup]

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