English
For a family of spaces X_i and s_i ⊆ X_i, and x ∈ ∏ X_i, the neighborhood filter of x in the restricted pi-space equals bottom precisely when some coordinate has an empty neighborhood within its s_i: 𝓝_{π I s}(x) = ⊥ iff ∃ i ∈ I with 𝓝_{s_i}(x_i) = ⊥.
Русский
Для семейства пространств X_i и множеств s_i ⊆ X_i, при x = (x_i) ∈ ∏ X_i фильтр окрестностей в ограниченном произведении π I s равен дну тогда и только тогда, когда для некоторой координаты i ∈ I окрестности x_i в s_i пусты.
LaTeX
$$$$\\\\mathcal{N}_{\\\\pi I s}(x) = \\\\bot \\\\iff \\\\exists i \\\\in I, \\\\mathcal{N}_{s_i}(x_i) = \\\\bot.$$$$
Lean4
theorem nhdsWithin_pi_eq_bot {I : Set ι} {s : ∀ i, Set (X i)} {x : ∀ i, X i} :
𝓝[pi I s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥ := by simp only [nhdsWithin, nhds_pi, pi_inf_principal_pi_eq_bot]
