toMultiset_eq_iff

Mathlib.Data.Finsupp.Multiset

URI: https://scilib.ai/kg/mathlib#Finsupp.toMultiset_eq_iff

← MathLib Explorer

English

For any f and s, toMultiset f = s if and only if f = toFinsupp s.

Русский

Для любых f и s: toMultiset f = s тогда и только тогда, когда f = toFinsupp s.

LaTeX

$$$\mathrm{toMultiset}(f) = s \;\iff\; f = \mathrm{toFinsupp}(s)$$$

Lean4

theorem toMultiset_eq_iff [DecidableEq α] {f : α →₀ ℕ} {s : Multiset α} :
    Finsupp.toMultiset f = s ↔ f = Multiset.toFinsupp s :=
  Multiset.toFinsupp.symm_apply_eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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