upperBounds_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem upperBounds_Ico {a b : γ} (hab : a < b) : upperBounds (Ico a b) = Ici b :=
  (isLUB_Ico hab).upperBounds_eq

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