prod_mem_nhds_iff — Mathlib

English

In a product space, a rectangle s × t belongs to the neighborhood of (x,y) if and only if s belongs to 𝓝 x and t belongs to 𝓝 y.

Русский

В произведении: прямоугольник s × t принадлежит окрестности (x,y) тогда, когда s ∈ 𝓝 x и t ∈ 𝓝 y.

LaTeX

$$$ s \\timesˢ t \\in 𝓝 (x, y) \\iff s \\in 𝓝 x \\land t \\in 𝓝 y $$$

Lean4

theorem prod_mem_nhds_iff {s : Set X} {t : Set Y} {x : X} {y : Y} : s ×ˢ t ∈ 𝓝 (x, y) ↔ s ∈ 𝓝 x ∧ t ∈ 𝓝 y := by
  rw [nhds_prod_eq, prod_mem_prod_iff]

Похожие утверждения