frontier_Iio'

Mathlib.Topology.Order.DenselyOrdered

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

English

If there exists points below a, the frontier of the open interval (−∞, a) is {a}.

Русский

Если существуют точки ниже a, граница интервала (−∞, a) равна {a}.

LaTeX

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

Lean4

@[simp]
theorem frontier_Iio' {a : α} (ha : (Iio a).Nonempty) : frontier (Iio a) = { a } := by simp [frontier, closure_Iio' ha]

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

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

Разделы

Аффилиация

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