closure_Ici

Mathlib.Topology.Order.OrderClosed

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

English

The closure of the ray Ici a equals itself; the ray [a, ∞) is closed.

Русский

Замыкание луча Ici a совпадает с самим Ici a; интервал [a, ∞) замкнут.

LaTeX

$$$ closure(Ici\, a) = Ici\, a $$$

Lean4

@[simp]
theorem closure_Ici (a : α) : closure (Ici a) = Ici a :=
  isClosed_Ici.closure_eq

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

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

Разделы

Аффилиация

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