isLUB_Ioc

Mathlib.Order.Bounds.Basic

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

English

Let a < b. The least upper bound of the half-open interval (a,b] is b; i.e., IsLUB(Ioc(a,b), b).

Русский

Пусть a < b. Наименьшее верхнее ограничение множества (a,b] равно b.

LaTeX

$$$a < b \implies \operatorname{IsLUB}(\\mathrm{Ioc}(a,b), b).$$$

Lean4

theorem isLUB_Ioc (h : a < b) : IsLUB (Ioc a b) b :=
  (isGreatest_Ioc h).isLUB

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

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

Разделы

Аффилиация

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