isLocallyClosed_Ioc

Mathlib.Topology.Order.IsLocallyClosed

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

← MathLib Explorer

English

The half-open interval Ioc(a,b) is locally closed in a space with ClosedIic topology.

Русский

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

LaTeX

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

Lean4

theorem isLocallyClosed_Ioc [LinearOrder X] [ClosedIicTopology X] : IsLocallyClosed (Set.Ioc a b) :=
  by
  rw [← Set.Iic_inter_Ioi]
  exact isLocallyClosed_Iic.inter isLocallyClosed_Ioi

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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