Intervals are locally closed

We prove that the intervals on a topological ordered space are locally closed.

theorem isLocallyClosed_Icc {X : Type u_1} [TopologicalSpace X] {a b : X} [Preorder X] [OrderClosedTopology X] : IsLocallyClosed (Set.Icc a b)

theorem isLocallyClosed_Ioo {X : Type u_1} [TopologicalSpace X] {a b : X} [LinearOrder X] [OrderClosedTopology X] : IsLocallyClosed (Set.Ioo a b)

theorem isLocallyClosed_Ici {X : Type u_1} [TopologicalSpace X] {a : X} [Preorder X] [ClosedIciTopology X] : IsLocallyClosed (Set.Ici a)

theorem isLocallyClosed_Iic {X : Type u_1} [TopologicalSpace X] {a : X} [Preorder X] [ClosedIicTopology X] : IsLocallyClosed (Set.Iic a)

theorem isLocallyClosed_Ioi {X : Type u_1} [TopologicalSpace X] {a : X} [LinearOrder X] [ClosedIicTopology X] : IsLocallyClosed (Set.Ioi a)

theorem isLocallyClosed_Iio {X : Type u_1} [TopologicalSpace X] {a : X} [LinearOrder X] [ClosedIciTopology X] : IsLocallyClosed (Set.Iio a)

theorem isLocallyClosed_Ioc {X : Type u_1} [TopologicalSpace X] {a b : X} [LinearOrder X] [ClosedIicTopology X] : IsLocallyClosed (Set.Ioc a b)

theorem isLocallyClosed_Ico {X : Type u_1} [TopologicalSpace X] {a b : X} [LinearOrder X] [ClosedIciTopology X] : IsLocallyClosed (Set.Ico a b)