toMultiset_inj

Mathlib.Data.DFinsupp.Multiset

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

English

The inj version for toMultiset: toMultiset f = toMultiset g iff f = g.

Русский

Инъекция для toMultiset: toMultiset f = toMultiset g эквивалентно f = g.

LaTeX

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

Lean4

@[simp]
theorem toMultiset_inj : toMultiset f = toMultiset g ↔ f = g :=
  toMultiset_injective.eq_iff

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

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

Разделы

Аффилиация

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