empty_ne_univ

Mathlib.Data.Set.Basic

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

English

If α is nonempty, then ∅ ≠ univ.

Русский

Если множество α непусто, то ∅ не равно univ.

LaTeX

$$$[\mathrm{Nonempty} \ \alpha] \;:\; (\emptyset : \mathrm{Set} \alpha) \neq \mathrm{univ}$$$

Lean4

theorem empty_ne_univ [Nonempty α] : (∅ : Set α) ≠ univ := fun e =>
  not_isEmpty_of_nonempty α <| univ_eq_empty_iff.1 e.symm

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

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

Разделы

Аффилиация

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