upperBounds_Ioo — Mathlib

English

Let a < b in a densely ordered semilattice with infimum. Then the upper bounds of Ioo(a,b) are exactly {x | x ≥ b}.

Русский

Пусть a < b в плотно упорядоченном полупространстве с инфимумом. Верхние границы Ioo(a,b) равны {x | x ≥ b}.

LaTeX

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

Lean4

theorem upperBounds_Ioo {a b : γ} (hab : a < b) : upperBounds (Ioo a b) = Ici b :=
  (isLUB_Ioo hab).upperBounds_eq

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