English
If a ≠ b in a densely ordered space, the closure of the interior of the closed interval [a,b] is exactly [a,b].
Русский
Для a ≠ b в плотно упорядоченном пространстве замыкание interior([a,b]) равно [a,b].
LaTeX
$$$\overline{\operatorname{int}(\mathrm{Icc}(a,b))} = \mathrm{Icc}(a,b)$$$
Lean4
theorem closure_interior_Icc {a b : α} (h : a ≠ b) : closure (interior (Icc a b)) = Icc a b :=
(closure_minimal interior_subset isClosed_Icc).antisymm <|
calc
Icc a b = closure (Ioo a b) := (closure_Ioo h).symm
_ ⊆ closure (interior (Icc a b)) := closure_mono (interior_maximal Ioo_subset_Icc_self isOpen_Ioo)