nhdsSet_Ioo — Mathlib

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

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