top_nonempty

Mathlib.Order.Notation

URI: https://scilib.ai/kg/mathlib#top_nonempty

English

If a type α has a top element, then α is nonempty.

Русский

Если у типа α есть верхняя граница, то α непустой.

LaTeX

$$$\operatorname{Nonempty}(\alpha)$$$

Lean4

instance (priority := 100) top_nonempty (α : Type*) [Top α] : Nonempty α :=
  ⟨⊤⟩

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

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

Разделы

Аффилиация

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