lowerBounds_Icc — Mathlib

English

Let a ≤ b. The set of lower bounds of the closed interval [a,b] is the ray (-∞, a], i.e., lowerBounds([a,b]) = Iic(a).

Русский

Пусть a ≤ b. Множество нижних границ замкнутого промежутка [a,b] равно лучу (-∞, a], то есть lowerBounds(Icc(a,b)) = Iic(a).

LaTeX

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

Lean4

theorem lowerBounds_Icc (h : a ≤ b) : lowerBounds (Icc a b) = Iic a :=
  (isGLB_Icc h).lowerBounds_eq

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