frontier_Iic'

Mathlib.Topology.Order.DenselyOrdered

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

English

If there exists points above a, the frontier of the left-closed ray (−∞, a] is {a}.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem frontier_Iic' {a : α} (ha : (Ioi a).Nonempty) : frontier (Iic a) = { a } := by simp [frontier, ha]

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

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

Разделы

Аффилиация

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