interior_Ici'

Mathlib.Topology.Order.DenselyOrdered

URI: https://scilib.ai/kg/mathlib#interior_Ici'

← MathLib Explorer

English

If Iio a is nonempty, interior of Ici a equals Ioi a.

Русский

Если Iio a непусто, interior([a, ∞)) = (a, ∞).

LaTeX

$$$ (Iio(a)).Nonempty \Rightarrow \operatorname{Interior}(Ici(a)) = Ioi(a) $$$

Lean4

@[simp]
theorem interior_Ici' {a : α} (ha : (Iio a).Nonempty) : interior (Ici a) = Ioi a := by
  rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]

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

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

Разделы

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

Аффилиация

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