closure_Ioi' — Mathlib

English

The closure of Ioi a equals Ici a whenever (Ioi a) is nonempty.

Русский

Замыкание интервала (a, ∞) равно [a, ∞) при непустом (Ioi a).

LaTeX

$$$ (Ioi(a)).Nonempty \Rightarrow \operatorname{closure}(Ioi(a)) = Ici(a) $$$

Lean4

/-- The closure of the interval `(a, +∞)` is the closed interval `[a, +∞)`, unless `a` is a top
element. -/
theorem closure_Ioi' {a : α} (h : (Ioi a).Nonempty) : closure (Ioi a) = Ici a :=
  by
  apply Subset.antisymm
  · exact closure_minimal Ioi_subset_Ici_self isClosed_Ici
  · rw [← diff_subset_closure_iff, Ici_diff_Ioi_same, singleton_subset_iff]
    exact isGLB_Ioi.mem_closure h

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