closure_Iio

Mathlib.Topology.Order.DenselyOrdered

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

← MathLib Explorer

English

The closure of Iio a equals Iic a for spaces with a minimal element absent.

Русский

Замыкание Iio a равно Iic a в отсутствии минимального элемента.

LaTeX

$$$ closure(Iio(a)) = Iic(a) $$$

Lean4

/-- The closure of the interval `(-∞, a)` is the interval `(-∞, a]`. -/
@[simp]
theorem closure_Iio (a : α) [NoMinOrder α] : closure (Iio a) = Iic a :=
  closure_Iio' nonempty_Iio

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

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

Разделы

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

Аффилиация

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