toFinset_eq_empty

Mathlib.Data.Finset.Basic

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

English

For any multiset m, m.toFinset is empty if and only if m is zero.

Русский

Для мультисета m, m.toFinset пустой тогда и только тогда, когда m = 0.

LaTeX

$$$m.toFinset = \\emptyset \\iff m = 0$$$

Lean4

@[simp]
theorem toFinset_eq_empty {m : Multiset α} : m.toFinset = ∅ ↔ m = 0 :=
  Finset.val_inj.symm.trans Multiset.dedup_eq_zero

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

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

Разделы

Аффилиация

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