toMultiset_injective

Mathlib.Data.DFinsupp.Multiset

URI: https://scilib.ai/kg/mathlib#DFinsupp.toMultiset_injective

English

toMultiset is injective: f = g if toMultiset f = toMultiset g.

Русский

toMultiset инъективно: если toMultiset f = toMultiset g, то f = g.

LaTeX

$$$$ \\operatorname{toMultiset} \\;f = \\operatorname{toMultiset} \\;g \\iff f = g $$$$

Lean4

theorem toMultiset_injective : Injective (toMultiset : (Π₀ _a, ℕ) → Multiset α) :=
  Multiset.equivDFinsupp.symm.injective

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

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

Разделы

Аффилиация

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