English
For any a and any subset s of α, the left and right nhds within s of a together equal the nhds of a within s with a removed; i.e., the union of 𝓝[s ∩ Iio a] a and 𝓝[s ∩ Ioi a] a equals 𝓝[s \ { a }] a.
Русский
Для любых a и множества s⊆α объединение окрестностей внутри s слева от a и внутри s справа от a дает окрестности в a внутри s без точки a; то есть 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ { a }] a.
LaTeX
$$$\mathcal{N}_{s \cap Iio(a)}(a) \sqcup \mathcal{N}_{s \cap Ioi(a)}(a) = \mathcal{N}_{s \setminus \{a\}}(a)$$$
Lean4
theorem nhdsWithinLT_sup_nhdsWithinGT (a : α) : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ { a }] a := by
rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff, inter_sdiff_left_comm,
univ_inter]
