mem_nhdsWithin_prod_iff — Mathlib

English

In a product, a subset s is in the neighborhood of (x,y) relative to tx ×ˢ ty if and only if there exist u ∈ 𝓝[tx] x and v ∈ 𝓝[ty] y with u ×ˢ v ⊆ s.

Русский

Для произведения, множество s принадлежит окрестности 𝓝[tx ×ˢ ty] (x,y) тогда, когда существуют u ∈ 𝓝[tx] x и v ∈ 𝓝[ty] y такие, что u ×ˢ v ⊆ s.

LaTeX

$$$ s ∈ 𝓝[tx ×ˢ ty] (x, y) \\iff \\exists u \\in 𝓝[tx] x, \\exists v \\in 𝓝[ty] y, u ×ˢ v ⊆ s $$$

Lean4

theorem mem_nhdsWithin_prod_iff {x : X} {y : Y} {s : Set (X × Y)} {tx : Set X} {ty : Set Y} :
    s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s := by rw [nhdsWithin_prod_eq, mem_prod_iff]

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