closure_Ico — Mathlib

English

If a ≠ b, the closure of Ioc a b is Icc a b.

Русский

Если a ≠ b, замыкание Ioc(a,b) равно Icc(a,b).

LaTeX

$$$ hab : a \neq b \Rightarrow closure(Ioc(a,b)) = Icc(a,b) $$$

Lean4

/-- The closure of the interval `[a, b)` is the closed interval `[a, b]`. -/
@[simp]
theorem closure_Ico {a b : α} (hab : a ≠ b) : closure (Ico a b) = Icc a b :=
  by
  apply Subset.antisymm
  · exact closure_minimal Ico_subset_Icc_self isClosed_Icc
  · apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)
    rw [closure_Ioo hab]

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