frontier_Ioo

Mathlib.Topology.Order.DenselyOrdered

URI: https://scilib.ai/kg/mathlib#frontier_Ioo

← MathLib Explorer

English

For a<b, the frontier of the open interval Ioo(a,b) is {a,b}.

Русский

Для a<b граница открытого интервала Ioo(a,b) равна {a,b}.

LaTeX

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

Lean4

@[simp]
theorem frontier_Ioo {a b : α} (h : a < b) : frontier (Ioo a b) = { a, b } := by
  rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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