lowerBounds_Ico

Mathlib.Order.Bounds.Basic

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

English

Let a < b. The set of lower bounds of [a,b) is {x | x ≤ a}; i.e., lowerBounds(Ico(a,b)) = Iic(a).

Русский

Пусть a < b. Множество нижних границ [a,b) равно {x | x ≤ a}; то есть lowerBounds(Ico(a,b)) = Iic(a).

LaTeX

$$$a < b \implies \operatorname{lowerBounds}(\\mathrm{Ico}(a,b)) = \\mathrm{Iic}(a).$$$

Lean4

theorem lowerBounds_Ico (h : a < b) : lowerBounds (Ico a b) = Iic a :=
  (isGLB_Ico h).lowerBounds_eq

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

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

Разделы

Аффилиация

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