English
In a product space X × Y, a subset s containing (x,y) is a neighborhood of (x,y) if and only if it contains a product of neighborhoods of x and y, i.e., s ∈ 𝓝(x,y) iff there exist u ∈ 𝓝 x and v ∈ 𝓝 y with u × v ⊆ s.
Русский
В пространстве X × Y подмножество s, содержащее (x,y), является окрестностью (x,y) тогда и только тогда, когда оно содержит произведение окрестностей x и y: s ∈ 𝓝(x,y) эквивалентно ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y такие, что u × v ⊆ s.
LaTeX
$$$ s \\in 𝓝 (x, y) \\iff \\exists u \\in 𝓝 x, \\exists v \\in 𝓝 y, u \\timesˢ v \\subseteq s $$$
Lean4
theorem mem_nhds_prod_iff {x : X} {y : Y} {s : Set (X × Y)} : s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s := by
rw [nhds_prod_eq, mem_prod_iff]
