BddAbove

Mathlib.Order.Bounds.Defs

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

English

A set is bounded above if there exists an upper bound.

Русский

Множество ограничено сверху, если существует верхняя грань.

LaTeX

$$$\\text{BddAbove}(s) \\iff \\exists x\\, \\forall a\\in s,\ a \\le x$$$

Lean4

/-- A set is bounded above if there exists an upper bound. -/
def BddAbove (s : Set α) :=
  (upperBounds s).Nonempty

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

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

Разделы

Аффилиация

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