English
Let a < b in a structure with semilattice-sup and dense order. Then a is the greatest lower bound of the open interval Ioo(a,b).
Русский
Пусть a < b в структуре с полуконечными верхними пределами и плотной упорядоченностью. Тогда a является наибольшей нижней границей открытого интервала Ioo(a,b).
LaTeX
$$$a < b \implies \text{IsGLB}(\\mathrm{Ioo}(a,b), a).$$$
Lean4
theorem isGLB_Ioo {a b : γ} (h : a < b) : IsGLB (Ioo a b) a :=
⟨fun _ hx => hx.1.le, fun x hx =>
by
rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂
· exact h₁.symm ▸ le_sup_left
obtain ⟨y, lty, ylt⟩ := exists_between h₂
apply (not_lt_of_ge (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim
obtain ⟨u, au, ub⟩ := exists_between h
apply (hx ⟨au, ub⟩).trans ub.le⟩
