eq_empty_or_nonempty

Mathlib.Data.Set.Basic

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

English

For any set s, either s is empty or s is nonempty.

Русский

Для любого множества s либо пусто, либо непусто.

LaTeX

$$$$ s = \emptyset \lor s.Nonempty. $$$$

Lean4

theorem eq_empty_or_nonempty (s : Set α) : s = ∅ ∨ s.Nonempty :=
  or_iff_not_imp_left.2 nonempty_iff_ne_empty.2

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

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

Разделы

Аффилиация

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