frontier_Ici'

Mathlib.Topology.Order.DenselyOrdered

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

English

If there exist points below a, the frontier of the ray [a, ∞) is {a}.

Русский

Если существуют точки меньшие a, граница луча [a, ∞) равна {a}.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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