empty_toList

Mathlib.Data.Multiset.Basic

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

English

The toList of s is empty if and only if s is empty (zero).

Русский

toList(s) пустой ⇔ s пусто (равно нулю).

LaTeX

$$$s.toList.isEmpty \\iff s = 0$$$

Lean4

theorem empty_toList {s : Multiset α} : s.toList.isEmpty ↔ s = 0 := by simp

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

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

Разделы

Аффилиация

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