interior_Ici

Mathlib.Topology.Order.DenselyOrdered

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

English

In a densely ordered space with no minimum, interior of Ici a equals Ioi a.

Русский

В плотнопорядковом пространстве без минимального элемента interior([a, ∞)) = (a, ∞).

LaTeX

$$$ [NoMinOrder \ α] \Rightarrow \operatorname{Interior}(Ici(a)) = Ioi(a) $$$

Lean4

theorem interior_Ici [NoMinOrder α] {a : α} : interior (Ici a) = Ioi a :=
  interior_Ici' nonempty_Iio

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

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

Разделы

Аффилиация

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