nhdsWithin_Iio_self_neBot'

Mathlib.Topology.Order.DenselyOrdered

URI: https://scilib.ai/kg/mathlib#nhdsWithin_Iio_self_neBot'

English

For a densely ordered space with no endpoints, the boundary of [a,b] equals {a,b} when a ≤ b.

Русский

В плотно упорядоченном пространстве без концов граница [a,b] равна {a,b} при a ≤ b.

LaTeX

$$$\operatorname{frontier}(\mathrm{Icc}(a,b)) = \{a,b\}$$$

Lean4

theorem nhdsWithin_Iio_self_neBot' {b : α} (H : (Iio b).Nonempty) : NeBot (𝓝[<] b) :=
  nhdsWithin_Iio_neBot' H (le_refl b)

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

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

Разделы

Аффилиация

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