English
Let X be a linearly ordered topological space with ClosedIci topology. Then the half-open interval Ico(a, b) is locally closed; that is, there exist an open set U and a closed set F in X such that Ico(a, b) = U ∩ F.
Русский
Пусть X — линейно упорядоченное топологическое пространство с топологией ClosedIci. Тогда полуоткрытое множество Ico(a, b) локально замкнуто: существуют открытое множество U и замкнутое множество F такие, что Ico(a, b) = U ∩ F.
LaTeX
$$$\\exists U\\,F,\\ IsOpen(U) \\wedge IsClosed(F) \\wedge \\mathrm{Ico}(a,b) = U \\cap F$$$
Lean4
theorem isLocallyClosed_Ico [LinearOrder X] [ClosedIciTopology X] : IsLocallyClosed (Set.Ico a b) :=
by
rw [← Set.Iio_inter_Ici]
exact isLocallyClosed_Iio.inter isLocallyClosed_Ici
