nonempty — Mathlib

English

If α is nonempty, then the universal set of α is a nonempty element (instance).

Русский

Если α непуст, то универсальное множество α является непустым элементом (инстанцией).

LaTeX

$$$$ [\text{Nonempty } \alpha] \Rightarrow \operatorname{Nonempty}(\mathrm{univ} : \mathrm{Set}\,\alpha). $$$$

Lean4

instance nonempty [Nonempty α] : Nonempty (↥(Set.univ : Set α)) :=
  Set.univ_nonempty.to_subtype

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