univ_nonempty

Mathlib.Data.Set.Basic

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

English

Let α be a type. If α is nonempty, then the universal set of α is nonempty.

Русский

Пусть α — тип. Если α непуст, то универсальное множество α непусто.

LaTeX

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

Lean4

@[simp]
theorem univ_nonempty : ∀ [Nonempty α], (univ : Set α).Nonempty
  | ⟨x⟩ => ⟨x, trivial⟩

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

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

Разделы

Аффилиация

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