isLUB_Ioo — Mathlib

English

In a densely ordered semilattice with infimum, the dual statement gives that IsLUB(Ioo(a,b), b) holds when a < b.

Русский

В плотно упорядоченном полупространстве с инфимумом двойственное утверждение дает, что IsLUB(Ioo(a,b), b) выполняется при a < b.

LaTeX

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

Lean4

theorem isLUB_Ioo {a b : γ} (hab : a < b) : IsLUB (Ioo a b) b := by simpa only [Ioo_toDual] using isGLB_Ioo hab.dual

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