toDFinsupp_inj

Mathlib.Data.DFinsupp.Multiset

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

English

Equivalence of equality tests: toDFinsupp s = toDFinsupp t iff s = t (simp).

Русский

Эквивалентность тестов равенства: toDFinsupp s = toDFinsupp t эквивает s = t (simp).

LaTeX

$$$$ \\bigl(toDFinsupp\, s = toDFinsupp\, t\\bigr) \\iff s = t $$$$

Lean4

@[simp]
theorem toDFinsupp_inj : toDFinsupp s = toDFinsupp t ↔ s = t :=
  toDFinsupp_injective.eq_iff

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

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

Разделы

Аффилиация

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