isGLB_Ioc_of_isGLB_Ioi — Mathlib

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

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