isLocallyClosed_Ioo

Mathlib.Topology.Order.IsLocallyClosed

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

English

In a linear order with order-closed topology, the open interval Ioo(a,b) is locally closed.

Русский

Открытый интервал локально замкнут в линейном порядке.

LaTeX

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

Lean4

theorem isLocallyClosed_Ioo [LinearOrder X] [OrderClosedTopology X] : IsLocallyClosed (Set.Ioo a b) :=
  isOpen_Ioo.isLocallyClosed

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

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

Разделы

Аффилиация

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