English
If nhds x has a basis with pX and sx, and nhds y has a basis with pY and sy, then nhds(x,y) has a basis with pX i.1 ∧ pY i.2 and sx i.1 ×ˢ sy i.2.
Русский
Если окрестности x имеют базис с pX и sx, а окрестности y имеют базис с pY и sy, то окрестности (x,y) имеют базис с pX i.1 ∧ pY i.2 и sx i.1 ×ˢ sy i.2.
LaTeX
$$$ (\\mathcal{N} x).HasBasis pX sx \\to (\\mathcal{N} y).HasBasis pY sy \\to (\\mathcal{N} (x, y)).HasBasis (fun i => pX i.fst ∧ pY i.snd) (fun i => sx i.fst ×ˢ sy i.snd) $$$
Lean4
theorem prod_nhds' {ιX ιY : Type*} {pX : ιX → Prop} {pY : ιY → Prop} {sx : ιX → Set X} {sy : ιY → Set Y} {p : X × Y}
(hx : (𝓝 p.1).HasBasis pX sx) (hy : (𝓝 p.2).HasBasis pY sy) :
(𝓝 p).HasBasis (fun i : ιX × ιY => pX i.1 ∧ pY i.2) fun i => sx i.1 ×ˢ sy i.2 :=
hx.prod_nhds hy
