upperBounds_Ioc — Mathlib

English

Let a < b. The upper bounds of the interval (a,b] are exactly the elements x with x ≥ b; i.e., upperBounds(Ioc(a,b)) = Ici(b).

Русский

Пусть a < b. Верхние границы интервала (a,b] равны всем x, удовлетворяющим x ≥ b; то есть upperBounds(Ioc(a,b)) = Ici(b).

LaTeX

$$$a < b \implies \operatorname{upperBounds}(\\mathrm{Ioc}(a,b)) = \\mathrm{Ici}(b).$$$

Lean4

theorem upperBounds_Ioc (h : a < b) : upperBounds (Ioc a b) = Ici b :=
  (isLUB_Ioc h).upperBounds_eq

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