nontrivial_of_nonempty

Mathlib.Data.Set.Basic

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

English

If α is nonempty, the power set is nontrivial; ∅ ≠ univ.

Русский

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

LaTeX

$$[Nonempty α] ⇒ \text{Nontrivial}(\mathrm{Set} \ α)$$

Lean4

instance nontrivial_of_nonempty [Nonempty α] : Nontrivial (Set α) :=
  ⟨⟨∅, univ, empty_ne_univ⟩⟩

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

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

Разделы

Аффилиация

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