English
Let α be a linearly ordered topological space. Then the join of the left-neighborhood filter at a and the right-neighborhood filter at a equals the neighborhood filter at a excluding the point a; i.e. the union of neighborhoods coming from the left and from the right covers every punctured neighborhood of a.
Русский
Пусть α — линейно упорядоченное топологическое множество. Тогда объединение фильтров окрестностей слева от a и справа от a образует фильтр окрестностей вокруг a, исключая саму точку a; т.е. окрестности слева и справа покрывают любую окрестность a без точки a.
LaTeX
$$$\mathcal{N}_{[<]}(a) \sqcup \mathcal{N}_{[>]}(a) = \mathcal{N}_{[\\neq]}(a)$$$
Lean4
theorem nhdsLT_sup_nhdsGT (a : α) : 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a := by rw [← nhdsWithin_union, Iio_union_Ioi]
