punctured_nhds_eq_nhdsWithin_sup_nhdsWithin

English

In a linear order, the punctured neighborhood at x equals the supremum of the left and right neighborhoods at x.

Русский

В линейном порядке для точки x окрестность без самой точки равна наибольшему объединению левой и правой окрестностей в точке x.

LaTeX

$$$$ 𝓝_{x \\neq}(x) = 𝓝_{x<}(x) \\sqcup 𝓝_{x>}(x) $$$$

Lean4

/-- Writing a punctured neighborhood filter as a sup of left and right filters. -/
theorem punctured_nhds_eq_nhdsWithin_sup_nhdsWithin [LinearOrder α] {x : α} : 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x := by
  rw [← Iio_union_Ioi, nhdsWithin_union]

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