bddBelow_Ioc

Mathlib.Order.Bounds.Basic

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

English

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

Русский

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

LaTeX

$$$ BddBelow(\ Ioc\ a\ b\ ) $$$

Lean4

@[simp]
theorem bddBelow_Ioc : BddBelow (Ioc a b) :=
  bddBelow_Icc.mono Ioc_subset_Icc_self

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

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

Разделы

Аффилиация

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