isLocallyClosed_Iio

Mathlib.Topology.Order.IsLocallyClosed

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

English

The open-interval Iio(a) is locally closed in a space with ClosedIciTopology.

Русский

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

LaTeX

$$$$\text{IsLocallyClosed}(\operatorname{Iio}(a)).$$$$

Lean4

theorem isLocallyClosed_Iio [LinearOrder X] [ClosedIciTopology X] : IsLocallyClosed (Set.Iio a) :=
  isOpen_Iio.isLocallyClosed

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

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

Разделы

Аффилиация

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