English
Let X_i be topological spaces indexed by i in a finite set I. For each i, let s_i ⊆ X_i and let x ∈ ∏_{i∈I} X_i with components x_i. Then the neighborhood filter of x in the restricted product ∏_{i} s_i equals the infimum of the pullbacks of the coordinate neighborhood filters: 𝓝_{π univ s}(x) = ⨅_{i} comap (π_i) (𝓝_{s_i}(x_i)).
Русский
Пусть I конечно; для каждой i дано топологическое пространство X_i и множества s_i ⊆ X_i. Пусть x = (x_i) ∈ ∏_{i∈I} X_i. Тогда окрестности точки x в произведении, ограниченном по s, равны наименьшей нижней границе прообразов окрестностей в каждой координате: 𝓝_{π univ s}(x) = ⨅_{i} comap (π_i) (𝓝_{s_i}(x_i)).
LaTeX
$$$\\\\mathcal{N}_{\\\\pi(\\\\mathrm{univ}, s)}(x) = \\\\bigwedge_{i} \\\\mathrm{comap}(\\\\pi_i)(\\\\mathcal{N}_{s_i}(x_i)).$$$
Lean4
theorem nhdsWithin_pi_univ_eq [Finite ι] (s : ∀ i, Set (X i)) (x : ∀ i, X i) :
𝓝[pi univ s] x = ⨅ i, comap (fun x => x i) (𝓝[s i] x i) := by
simpa [nhdsWithin] using nhdsWithin_pi_eq finite_univ s x
