toFinset_nonempty_iff

Mathlib.Data.Finset.Insert

URI: https://scilib.ai/kg/mathlib#List.toFinset_nonempty_iff

English

The nonemptiness of l.toFinset is equivalent to l ≠ [].

Русский

Не пустота l.toFinset эквивалентна l ≠ [].

LaTeX

$$$ l.toFinset \\ Nonempty \\iff l \\neq []. $$$

Lean4

@[simp]
theorem toFinset_nonempty_iff (l : List α) : l.toFinset.Nonempty ↔ l ≠ [] := by simp [Finset.nonempty_iff_ne_empty]

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

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

Разделы

Аффилиация

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