isGLB_Ico

Mathlib.Order.Bounds.Basic

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

English

Let a < b. The interval [a,b) has a as its greatest lower bound; i.e., infimum of Ico(a,b) is a.

Русский

Пусть a < b. Интервал [a,b) имеет a в качестве наибольшей нижней границы; то есть inf(Ico(a,b)) = a.

LaTeX

$$$a < b \implies \inf(\\mathrm{Ico}(a,b)) = a.$$$

Lean4

theorem isGLB_Ico (h : a < b) : IsGLB (Ico a b) a :=
  (isLeast_Ico h).isGLB

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

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

Разделы

Аффилиация

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