frontier_Ioi'

Mathlib.Topology.Order.DenselyOrdered

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

English

If (Ioi a) is nonempty, the frontier of the open ray (a, ∞) is {a}.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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