interior_Icc — Mathlib

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]

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