bddAbove

Mathlib.Topology.Order.Bornology

URI: https://scilib.ai/kg/mathlib#Bornology.IsBounded.bddAbove

English

If a set is bounded, it has an upper bound.

Русский

Если множество ограничено, у него есть верхняя граница.

LaTeX

$$$\operatorname{IsBounded}(s) \rightarrow \operatorname{BddAbove}(s)$$$

Lean4

protected theorem bddAbove (hs : IsBounded s) : BddAbove s :=
  (isBounded_iff_bddBelow_bddAbove.1 hs).2

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

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

Разделы

Аффилиация

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