coe_eq_zero_iff_isEmpty

Mathlib.Data.Multiset.ZeroCons

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

English

For any list l, (l as a multiset) equals zero if and only if l is empty.

Русский

Для любого списка l преобразование в мультисет равно нулю тогда, когда список пуст.

LaTeX

$$(l : Multiset α) = 0 \\iff l.isEmpty$$

Lean4

theorem coe_eq_zero_iff_isEmpty (l : List α) : (l : Multiset α) = 0 ↔ l.isEmpty :=
  Iff.trans (coe_eq_zero l) isEmpty_iff.symm

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

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

Разделы

Аффилиация

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