isGLB_univ

Mathlib.Order.Bounds.Basic

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

English

In a preorder with a bottom element, the greatest lower bound of the universe is the bottom element.

Русский

В упорядоченном порядке с нижней границей наибольшей нижней границей вселенной является ⊥.

LaTeX

$$$\\operatorname{IsGLB}(\\mathrm{univ}, \\bot)$$$

Lean4

theorem isGLB_univ [OrderBot α] : IsGLB (univ : Set α) ⊥ :=
  isLeast_univ.isGLB

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

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

Разделы

Аффилиация

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