upperBounds_Icc — Mathlib

English

Let a ≤ b. The upper bounds of the closed interval [a,b] are exactly the elements x with x ≥ b; i.e., upperBounds([a,b]) = [b, ∞).

Русский

Пусть a ≤ b. Верхние границы замкнутого промежутка [a,b] состоят ровно из элементов x, удовлетворяющих x ≥ b; то есть upperBounds(Icc(a,b)) = Ici(b).

LaTeX

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

Lean4

theorem upperBounds_Icc (h : a ≤ b) : upperBounds (Icc a b) = Ici b :=
  (isLUB_Icc h).upperBounds_eq

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