interior_Ioc — Mathlib

English

For spaces with no maximum, the interior of the half-open interval Ioc(a,b) equals the open interval Ioo(a,b).

Русский

В пространствах без максимального элемента interior(Ioc(a,b)) совпадает с открытым интервалом Ioo(a,b).

LaTeX

$$$\operatorname{int}(\mathrm{Ioc}(a,b)) = \mathrm{Ioo}(a,b)$$$

Lean4

@[simp]
theorem interior_Ioc [NoMaxOrder α] {a b : α} : interior (Ioc a b) = Ioo a b := by
  rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]

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