count_dedup — Mathlib

English

For any multiset m and element a, the count of a in dedup(m) is 1 if a is in m, and 0 otherwise.

Русский

Для любого мультимножества m и элемента a число вхождений a в dedup(m) равно 1, если a ∈ m, и 0 в противном случае.

LaTeX

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

Lean4

theorem count_dedup (m : Multiset α) (a : α) : m.dedup.count a = if a ∈ m then 1 else 0 :=
  Quot.induction_on m fun _ => by
    simp only [quot_mk_to_coe'', coe_dedup, mem_coe, coe_count]
    apply List.count_dedup _ _

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