count_eq_one_of_mem — Mathlib

English

If s is nodup, then for each a, count(a, s) = 1 if a ∈ s, and 0 otherwise.

Русский

Если s — без повторов, то для каждого a: count(a, s) = 1, если a ∈ s, иначе 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

@[simp]
theorem count_eq_one_of_mem [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) (h : a ∈ s) : count a s = 1 :=
  nodup_iff_count_eq_one.mp d a h

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