not_nonempty_empty

Mathlib.Data.Set.Basic

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

English

The empty set is not nonempty.

Русский

Пустое множество не является непустым.

LaTeX

$$$$ \text{not_nonempty_empty} : \neg (\emptyset : \mathrm{Set}\,\alpha).Nonempty. $$$$

Lean4

@[simp]
theorem not_nonempty_empty : ¬(∅ : Set α).Nonempty := fun ⟨_, hx⟩ => hx

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

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

Разделы

Аффилиация

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