nhdsWithin_prod_eq — Mathlib

English

Let X and Y be topological spaces, x ∈ X, y ∈ Y, and s ⊆ X, t ⊆ Y. Then the neighborhood of (x,y) within s × t is the product of the neighborhoods of x in s and y in t:

Русский

Пусть X и Y — пространства с топологиями, x ∈ X, y ∈ Y, и s ⊆ X, t ⊆ Y. Тогда окрестность (x,y) внутри s × t есть произведение окрестностей x в s и y в t:

LaTeX

$$$\\mathcal{N}_{s\\times t}(x,y) = \\mathcal{N}_{s}(x) \\times \\mathcal{N}_{t}(y)$$$

Lean4

theorem nhdsWithin_prod_eq (x : X) (y : Y) (s : Set X) (t : Set Y) : 𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y := by
  simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]

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