toDFinsupp_apply

Mathlib.Data.DFinsupp.Multiset

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

English

For each a, the a-th coordinate of toDFinsupp s equals s.count a.

Русский

Для каждого элемента a координата в toDFinsupp s равна count(a, s).

LaTeX

$$$$ \\bigl(\\operatorname{toDFinsupp} s\\bigr)(a) = \\operatorname{count}(a, s) $$$$

Lean4

@[simp]
theorem toDFinsupp_apply (s : Multiset α) (a : α) : Multiset.toDFinsupp s a = s.count a :=
  rfl

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

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

Разделы

Аффилиация

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