English
The restricted pi-neighborhood is nontrivial exactly when each coordinate’s restricted neighborhood is nontrivial: (nhdsWithin x (I.pi s)).NeBot ⇔ ∀ i ∈ I, (nhdsWithin (x_i) (s_i)).NeBot.
Русский
Окрестности в произведении с ограничением непусты тогда, когда каждая координата имеет непустые окрестности в своей ограниченной области: (nhdsWithin x (I.pi s)).NeBot ⇔ ∀ i ∈ I, (nhdsWithin (x_i) (s_i)).NeBot.
LaTeX
$$$$(\\\\mathcal{N}_{\\\\pi I s}(x)).NeBot \\\\iff \\\\forall i \\\\in I, (\\\\mathcal{N}_{s_i}(x_i)).NeBot.$$$$
Lean4
theorem nhdsWithin_pi_neBot {I : Set ι} {s : ∀ i, Set (X i)} {x : ∀ i, X i} :
(𝓝[pi I s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot := by simp [neBot_iff, nhdsWithin_pi_eq_bot]
