English
If for all i, nhdsWithin (x_i) (Iio (x_i)) is nontrivial, then nhdsWithin x (Iio x) is nontrivial; if nhdsWithin (x_i) (Ioi (x_i)) is nontrivial for all i, then nhdsWithin x (Ioi x) is nontrivial.
Русский
Если во всех координатах существуют непустые окрестности в Iio(x_i) или в Ioi(x_i), то в произведении непустые окрестности в соответствующих множествах Iio x и Ioi x.
LaTeX
$$$$ (\\\\mathcal{N}_{<}(x)).NeBot \\\\Rightarrow (\\\\mathcal{N}_{<} x).NeBot \\\\phantom{\\\\Rightarrow} \\\\text{ и } \\\\ (\\\\mathcal{N}_{>}(x)).NeBot \\\\Rightarrow (\\\\mathcal{N}_{> } x).NeBot. $$$$
Lean4
theorem piecewise_nhdsWithin {f g : α → β} {t : Set α} [∀ x, Decidable (x ∈ t)] {a : α} {s : Set α} {l : Filter β}
(h₀ : Tendsto f (𝓝[s ∩ t] a) l) (h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l) : Tendsto (piecewise t f g) (𝓝[s] a) l := by
apply Tendsto.piecewise <;> rwa [← nhdsWithin_inter']
