count_singleton — Mathlib

English

Let a and b be elements of a type. The multiplicity of a in the singleton multiset {b} is 1 if a = b and 0 otherwise.

Русский

Пусть a и b — элементы типа. Число вхождений a в единичное мультимножество {b} равно 1, если a = b, и 0 в противном случае.

LaTeX

$$$\operatorname{count}(a, \{b\}) = \begin{cases}1,& a=b\\0,& a\neq b\end{cases}$$$

Lean4

theorem count_singleton (a b : α) : count a ({ b } : Multiset α) = if a = b then 1 else 0 := by
  simp only [count_cons, ← cons_zero, count_zero, Nat.zero_add]

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