bot_nonempty

Mathlib.Order.Notation

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

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) bot_nonempty (α : Type*) [Bot α] : Nonempty α :=
  ⟨⊥⟩

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

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

Разделы

Аффилиация

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