English
In a densely ordered space with neither endpoint, interior of Icc a b equals Ioo a b.
Русский
В плотно упорядоченном пространстве без минимального и максимального элемента interior(Icc a b) = Ioo a b.
LaTeX
$$$ [NoMinOrder \ α] [NoMaxOrder \ α] \Rightarrow \operatorname{Interior}(Icc(a,b)) = Ioo(a,b) $$$
Lean4
@[simp]
theorem interior_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} : interior (Icc a b) = Ioo a b := by
rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]