interior_Iic

Mathlib.Topology.Order.DenselyOrdered

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

English

In a space with no maximum, interior of Iic a equals Iio a.

Русский

В пространстве без максимума interior(Iic a) = Iio a.

LaTeX

$$$ [NoMaxOrder \ α] \Rightarrow \operatorname{Interior}(Iic(a)) = Iio(a) $$$

Lean4

theorem interior_Iic [NoMaxOrder α] {a : α} : interior (Iic a) = Iio a :=
  interior_Iic' nonempty_Ioi

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

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

Разделы

Аффилиация

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