English
If i < j and k is the GLB of Ioi(i), then k is the GLB of Ioc(i, j).
Русский
Если i < j и k является наименьшей верхней границей множества Ioi(i), то k является наименьшей верхней границей множества Ioc(i, j).
LaTeX
$$$\\text{IsGLB}(\\{x:ι \\mid i < x\\}, k) \\Rightarrow \\text{IsGLB}(\\{x:ι \\mid i < x \\le j\\}, k)$$$
Lean4
theorem isGLB_Ioc_of_isGLB_Ioi {i j k : ι} (hij_lt : i < j) (h : IsGLB (Set.Ioi i) k) : IsGLB (Set.Ioc i j) k :=
by
simp_rw [IsGLB, IsGreatest, mem_upperBounds, mem_lowerBounds] at h ⊢
refine ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩
intro y hy
rcases le_or_gt y j with h_le | h_lt
· exact hx y ⟨hy, h_le⟩
· exact le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le