closure_Icc

Mathlib.Topology.Order.OrderClosed

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

English

The closure of Icc(a,b) equals Icc(a,b) in OrderClosedTopology; i.e., Icc is already closed.

Русский

Замкнутость множества Icc в OrderClosedTopology; closure(Icc(a,b)) = Icc(a,b).

LaTeX

$$$\mathrm{closure}(Icc(a,b)) = Icc(a,b)$$$

Lean4

@[simp]
theorem closure_Icc (a b : α) : closure (Icc a b) = Icc a b :=
  isClosed_Icc.closure_eq

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

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

Разделы

Аффилиация

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