not_empty_toList

Mathlib.Data.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.not_empty_toList

English

For any nonempty finset s, s.toList is not empty.

Русский

Для любого непустого финсета s список его элементов не пуст.

LaTeX

$$$ s\\\\.Nonempty \\\\rightarrow s\\\\.toList \\\\neq []$$$

Lean4

theorem not_empty_toList {s : Finset α} (hs : s.Nonempty) : ¬s.toList.isEmpty :=
  mt empty_toList.mp hs.ne_empty

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

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

Разделы

Аффилиация

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