isBounded_iff_bddBelow_bddAbove

Mathlib.Topology.Order.Bornology

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

English

IsBounded is equivalent to the conjunction of lower and upper boundedness.

Русский

Ограниченность эквивалентна союзу нижней и верхней ограниченности.

LaTeX

$$$\operatorname{IsBounded}(s) \iff (\operatorname{BddBelow}(s) \land \operatorname{BddAbove}(s))$$$

Lean4

theorem isBounded_iff_bddBelow_bddAbove : IsBounded s ↔ BddBelow s ∧ BddAbove s :=
  IsOrderBornology.isBounded_iff_bddBelow_bddAbove _

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

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

Разделы

Аффилиация

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