English
If nhds x has a basis indexed by ιX and sx, and nhds y has a basis indexed by ιY and sy, then nhds(x,y) has a basis indexed by ιX × ιY given by sx and sy via product sets.
Русский
Если окрестности x имеют базис, индексируемый ιX и наборы sx, а окрестности y — базис ιY и наборы sy, то окрестности (x,y) имеют базис, индексируемый ιX × ιY и состоящий из произведений sx i1 и sy i2.
LaTeX
$$$ (\\mathcal{N} (x)).HasBasis pX\\; sx \\; \\Rightarrow \\; (\\mathcal{N} (y)).HasBasis pY\\; sy \\Rightarrow \\\\ (\\mathcal{N} (x, y)).HasBasis (fun i => pX i.1 \\land pY i.2) (fun i => sx i.1 \\timesˢ sy i.2) $$$
Lean4
theorem prod_nhds {ιX ιY : Type*} {px : ιX → Prop} {py : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {x : X} {y : Y}
(hx : (𝓝 x).HasBasis px sx) (hy : (𝓝 y).HasBasis py sy) :
(𝓝 (x, y)).HasBasis (fun i : ιX × ιY => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2 :=
by
rw [nhds_prod_eq]
exact hx.prod hy
