toDFinsupp_injective

Mathlib.Data.DFinsupp.Multiset

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

English

toDFinsupp is injective: if toDFinsupp s = toDFinsupp t then s = t.

Русский

toDFinsupp инъективно: если toDFinsupp s = toDFinsupp t, тогда s = t.

LaTeX

$$$$ \\operatorname{toDFinsupp} \\, s = \\operatorname{toDFinsupp} \\, t \\iff s = t $$$$

Lean4

theorem toDFinsupp_injective : Injective (toDFinsupp : Multiset α → Π₀ _a, ℕ) :=
  equivDFinsupp.injective

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

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

Разделы

Аффилиация

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