isLocallyClosed_Icc

Mathlib.Topology.Order.IsLocallyClosed

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

English

In any topological space with a compatible preorder and order-closed topology, the closed interval Icc(a,b) is locally closed.

Русский

Замкнутый интервал локально замкнут.

LaTeX

$$$$\text{IsLocallyClosed}(\operatorname{Icc}(a,b)).$$$$

Lean4

theorem isLocallyClosed_Icc [Preorder X] [OrderClosedTopology X] : IsLocallyClosed (Set.Icc a b) :=
  isClosed_Icc.isLocallyClosed

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

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

Разделы

Аффилиация

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