bddBelow

Mathlib.Topology.Order.Bornology

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

English

If a set is bounded, it has a lower bound.

Русский

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

LaTeX

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

Lean4

protected theorem bddBelow (hs : IsBounded s) : BddBelow s :=
  (isBounded_iff_bddBelow_bddAbove.1 hs).1

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

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

Разделы

Аффилиация

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