English
For the open interval Ioo(a,b) in a linearly ordered topological space with OrderClosedTopology, the set of neighborhoods equals the principal filter on Ioo(a,b).
Русский
Для открытого отрезка Ioo(a,b) в линейном топологическом пространстве с OrderClosedTopology множество окрестностей совпадает с принципиальным фильтром на Ioo(a,b).
LaTeX
$$$𝓝^{s}(Ioo(a,b)) = 𝓟(Ioo(a,b))$$$
Lean4
@[simp]
theorem nhdsSet_Ioo : 𝓝ˢ (Ioo a b) = 𝓟 (Ioo a b) :=
isOpen_Ioo.nhdsSet_eq