not_nonempty_iff_eq_empty

Mathlib.Data.Set.Basic

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

← MathLib Explorer

English

Not nonempty is equivalent to being empty (variant).

Русский

Не-непусто эквивалентно пустоте (вариант).

LaTeX

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

Lean4

/-- See also `Set.nonempty_iff_ne_empty`. -/
@[push]
theorem not_nonempty_iff_eq_empty : ¬s.Nonempty ↔ s = ∅ := by
  simp only [Set.Nonempty, not_exists, eq_empty_iff_forall_notMem]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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