count

Mathlib.Data.Multiset.Count

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

English

The count of a in s is the multiplicity of a in s: count(a, s) = countP (a = ·) s.

Русский

Подсчет элемента a в s является его кратностью в s: count(a, s) = countP (a = ·) s.

LaTeX

$$$\operatorname{count}(a, s) = \operatorname{countP}(\lambda x. a = x, s)$$$

Lean4

/-- `count a s` is the multiplicity of `a` in `s`. -/
def count (a : α) : Multiset α → ℕ :=
  countP (a = ·)

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

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

Разделы

Аффилиация

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