bddAbove

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#IsLUB.bddAbove

English

If s has a least upper bound a, then s is bounded above.

Русский

Если s имеет наименьшую верхнюю грань a, то s ограничено сверху.

LaTeX

$$$IsLUB(s,a) \\rightarrow BddAbove(s)$$$

Lean4

/-- If `s` has a least upper bound, then it is bounded above. -/
theorem bddAbove (h : IsLUB s a) : BddAbove s :=
  ⟨a, h.1⟩

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

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

Разделы

Аффилиация

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