bddBelow_Ioi

Mathlib.Order.Bounds.Basic

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

English

The set {x > a} is bounded below; a is a lower bound.

Русский

Множество {x > a} ограничено снизу; a является нижней границей.

LaTeX

$$$BddBelow (Ioi a)$$$

Lean4

theorem bddBelow_Ioi : BddBelow (Ioi a) :=
  ⟨a, fun _ hx => le_of_lt hx⟩

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

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

Разделы

Аффилиация

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