toFinsupp_support

Mathlib.Data.Finsupp.Multiset

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

English

The support of the finsupp corresponding to a multiset equals its Finset of elements.

Русский

Опора функции finsupp, соответствующей мультимножество, совпадает с Finset элементов мультимножества.

LaTeX

$$$\mathrm{supp}(\mathrm{toFinsupp}(s)) = s_{\mathrm{toFinset}}$$$

Lean4

@[simp]
theorem toFinsupp_support (s : Multiset α) : s.toFinsupp.support = s.toFinset :=
  rfl

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

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

Разделы

Аффилиация

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