upperBounds_singleton

Mathlib.Order.Bounds.Basic

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

English

The set of upper bounds of {a} is equal to [a, ∞).

Русский

Множество верхних границ множества {a} равно [a, ∞).

LaTeX

$$$ upperBounds(\{ a \}) = \ Ici\ a $$$

Lean4

@[simp]
theorem upperBounds_singleton : upperBounds { a } = Ici a :=
  isLUB_singleton.upperBounds_eq

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

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

Разделы

Аффилиация

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