bddBelow_Ico

Mathlib.Order.Bounds.Basic

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

English

The half-open interval Ico(a,b) is bounded below by a.

Русский

Полуоткрытый интервал Ico(a,b) ограничен снизу a.

LaTeX

$$$ BddBelow(\ Ico\ a\ b\ ) $$$

Lean4

@[simp]
theorem bddBelow_Ico : BddBelow (Ico a b) :=
  bddBelow_Icc.mono Ico_subset_Icc_self

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

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

Разделы

Аффилиация

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