interior_Ico

Mathlib.Topology.Order.DenselyOrdered

URI: https://scilib.ai/kg/mathlib#interior_Ico

← MathLib Explorer

English

If a is well-ordered to the left, interior of Ico a b equals Ioo a b.

Русский

Если a слева ограничен, interior(Ico a b) = Ioo a b.

LaTeX

$$$ [NoMinOrder \ α] {a b : α} \Rightarrow \operatorname{Interior}(Ico(a,b)) = Ioo(a,b) $$$

Lean4

@[simp]
theorem interior_Ico [NoMinOrder α] {a b : α} : interior (Ico a b) = Ioo a b := by
  rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru