count_of — Mathlib

English

For x,y ∈ α, count x (of y) equals 1 if x=y and 0 otherwise, as an additive function.

Русский

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

LaTeX

$$$\\operatorname{count_of}(p)(x,y) = \\begin{cases} 1, & x=y \\\\ 0, & x\\neq y \\end{cases}$$$

Lean4

theorem count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y :=
  by
  dsimp [count]
  rw [countP_of]
  simp [Pi.single, Function.update]

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