isGLB_empty

Mathlib.Order.Bounds.Basic

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

English

There exists an IsGLB relation for the empty set with the top element: IsGLB empties with top.

Русский

С пустым множеством верхняя граница существует как топ-элемент: IsGLB ∅ ⊤.

LaTeX

$$$\\operatorname{IsGLB}(\\varnothing, \\top)$$$

Lean4

theorem isGLB_empty [OrderTop α] : IsGLB ∅ (⊤ : α) :=
  isGLB_empty_iff.2 isTop_top

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

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

Разделы

Аффилиация

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