count_eq_of_nodup — Mathlib

English

Let α be a type with decidable equality. If l is a list with no duplicates, then the number of occurrences of a in l equals 1 when a ∈ l, and 0 otherwise.

Русский

Пусть α — тип с разрешимым равенством. Если список l не содержит повторов, то число вхождений a в l равно 1, если a ∈ l, и 0 иначе.

LaTeX

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

Lean4

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

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