toList_ne_nil

Mathlib.Data.Finset.Basic

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

English

If a finset s is nonempty, then its toList is not the empty list.

Русский

Если финсет s непуст, то s.toList не равен пустому списку.

LaTeX

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

Lean4

theorem toList_ne_nil {s : Finset α} (hs : s.Nonempty) : s.toList ≠ [] :=
  mt toList_eq_nil.mp hs.ne_empty

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

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

Разделы

Аффилиация

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