instNonemptyTop

Mathlib.Data.Set.Basic

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

English

If α is nonempty, then the top set ⊤ in Set α is nonempty.

Русский

Если α непуст, то верхнее множество ⊤ в Set α непусто.

LaTeX

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

Lean4

instance instNonemptyTop [Nonempty α] : Nonempty (⊤ : Set α) :=
  inferInstanceAs (Nonempty (univ : Set α))

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

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

Разделы

Аффилиация

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