lowerBounds_Ioc

Mathlib.Order.Bounds.Basic

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

English

Let a < b. The interval (a,b] has a as its greatest lower bound.

Русский

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

LaTeX

$$$a < b \implies \text{GLB}(\\mathrm{Ioc}(a,b)) = a.$$$

Lean4

theorem lowerBounds_Ioc {a b : γ} (hab : a < b) : lowerBounds (Ioc a b) = Iic a :=
  (isGLB_Ioc hab).lowerBounds_eq

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

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

Разделы

Аффилиация

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