upperBounds_univ

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#NoTopOrder.upperBounds_univ

← MathLib Explorer

English

In a NoTopOrder, the set of upper bounds of the universe is empty.

Русский

В NoTopOrder множество верхних границ универсума пусто.

LaTeX

$$$\\operatorname{upperBounds}(\\mathrm{univ}) = \\emptyset$$$

Lean4

@[simp]
theorem upperBounds_univ [NoTopOrder α] : upperBounds (univ : Set α) = ∅ :=
  eq_empty_of_subset_empty fun b hb => not_isTop b fun x => hb (mem_univ x)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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