English
If a ≠ b, then closure(Ioo(a,b)) = Icc(a,b).
Русский
Если a ≠ b, то замыкание (a, b) равно [a, b].
LaTeX
$$$ Ne(a,b) \Rightarrow closure(Ioo(a,b)) = Icc(a,b) $$$
Lean4
/-- The closure of the open interval `(a, b)` is the closed interval `[a, b]`. -/
@[simp]
theorem closure_Ioo {a b : α} (hab : a ≠ b) : closure (Ioo a b) = Icc a b :=
by
apply Subset.antisymm
· exact closure_minimal Ioo_subset_Icc_self isClosed_Icc
· rcases hab.lt_or_gt with hab | hab
· rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le]
have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab
simp only [insert_subset_iff, singleton_subset_iff]
exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩
· rw [Icc_eq_empty_of_lt hab]
exact empty_subset _
