frontier_Iio

Mathlib.Topology.Order.DenselyOrdered

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

English

In NoMinOrder spaces, the frontier of Iio a equals {a} when Iio a is nonempty.

Русский

В пространствах без минимума граница Iio(a) равна {a} при непустом Iio a.

LaTeX

$$$ frontier(\mathrm{Iio}(a)) = \{a\}$$$

Lean4

theorem frontier_Iio [NoMinOrder α] {a : α} : frontier (Iio a) = { a } :=
  frontier_Iio' nonempty_Iio

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

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

Разделы

Аффилиация

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