count_cons

Mathlib.Data.Multiset.Count

URI: https://scilib.ai/kg/mathlib#Multiset.count_cons

English

The count of a in b :: s equals count a s plus 1 if a = b, else 0.

Русский

Подсчет элемента a в b :: s равен count a s плюс 1, если a = b, иначе 0.

LaTeX

$$$\operatorname{count}(a, (b ::ₘ s)) = \operatorname{count}(a, s) + \begin{cases}1, & a = b \\ 0, & \text{else} \end{cases}$$$

Lean4

theorem count_cons (a b : α) (s : Multiset α) : count a (b ::ₘ s) = count a s + if a = b then 1 else 0 :=
  countP_cons (a = ·) _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru