count_of — Mathlib

English

For x,y ∈ α, count x (of y) equals 1 if x = y and 0 otherwise, expressed in Multiplicative ℕ.

Русский

Для x,y ∈ α, count x (of y) равно 1, если x = y, и 0 иначе.

LaTeX

$$$\\operatorname{count}(x)(\\mathrm{of}(y)) = \\begin{cases} 1, & x = y \\\\ 0, & x \\neq y \\end{cases}$$$

Lean4

theorem count_of [DecidableEq α] (x y : α) :
    count x (of y) = Pi.mulSingle (M := fun _ => Multiplicative ℕ) x (Multiplicative.ofAdd 1) y := by
  simp only [count, eq_comm, countP_of, ofAdd_zero, Pi.mulSingle_apply]

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