isLUB_Ico — Mathlib

English

Let a < b. The half-open interval Ico(a,b) has b as its least upper bound; i.e., IsLUB(Ico(a,b), b).

Русский

Пусть a < b. Полуоткрытый интервал Ico(a,b) имеет b в качестве наименьшей верхней границы; то есть IsLUB(Ico(a,b), b).

LaTeX

$$$a < b \implies \text{IsLUB}(\\mathrm{Ico}(a,b), b).$$$

Lean4

theorem isLUB_Ico {a b : γ} (hab : a < b) : IsLUB (Ico a b) b := by simpa only [Ioc_toDual] using isGLB_Ioc hab.dual

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