not_nonempty_iff_eq_empty

Mathlib.Data.Finset.Empty

URI: https://scilib.ai/kg/mathlib#Finset.not_nonempty_iff_eq_empty

English

No Finset is nonempty iff it equals the empty Finset.

Русский

Никакой Finset не является непустым тогда, когда он равен пустому Finset.

LaTeX

$$$\\\\neg s.Nonempty \\\\iff s = \\\\emptyset$$$

Lean4

@[simp]
theorem not_nonempty_iff_eq_empty {s : Finset α} : ¬s.Nonempty ↔ s = ∅ :=
  nonempty_iff_ne_empty.not.trans not_not

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

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

Разделы

Аффилиация

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