nhdsWithin_Iio_neBot

Mathlib.Topology.Order.DenselyOrdered

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

English

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

Русский

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

LaTeX

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

Lean4

theorem nhdsWithin_Iio_neBot [NoMinOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Iio b] a) :=
  nhdsWithin_Iio_neBot' nonempty_Iio H

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

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

Разделы

Аффилиация

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