isBounded

Mathlib.Topology.Order.Bornology

URI: https://scilib.ai/kg/mathlib#BddBelow.isBounded

English

The conjunction of a lower and upper bound yields boundedness.

Русский

Сочетание нижней и верхней границ даёт ограниченность.

LaTeX

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

Lean4

protected theorem isBounded (hs₀ : BddBelow s) (hs₁ : BddAbove s) : IsBounded s :=
  isBounded_iff_bddBelow_bddAbove.2 ⟨hs₀, hs₁⟩

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

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

Разделы

Аффилиация

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