count_eq_of_nodup — Mathlib

English

If s is nodup, then for any a, count(a, s) = if a ∈ s then 1 else 0.

Русский

Если s — без повторов, то для любого a: count(a, s) = if a ∈ s then 1 else 0.

LaTeX

$$$\operatorname{Nodup}(s) \Rightarrow \forall a, \operatorname{count}(a, s) = \begin{cases}1,& a \in s \\ 0,& a \notin s\end{cases}$$$

Lean4

theorem count_eq_of_nodup [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) : count a s = if a ∈ s then 1 else 0 :=
  by
  split_ifs with h
  · exact count_eq_one_of_mem d h
  · exact count_eq_zero_of_notMem h

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