nhdsWithin_prod — Mathlib

English

If u is a neighborhood of a within s and v is a neighborhood of b within t, then u × v is a neighborhood of (a,b) within s × t.

Русский

Если u — окрестность a внутри s и v — окрестность b внутри t, то u × v — окрестность (a,b) внутри s × t.

LaTeX

$$$$ u \\in 𝓝[s] a \\; \\land \\; v \\in 𝓝[t] b \\Rightarrow u \\times\\! v \\in 𝓝[s \\times\\! t](a,b) $$$$

Lean4

theorem nhdsWithin_prod [TopologicalSpace β] {s u : Set α} {t v : Set β} {a : α} {b : β} (hu : u ∈ 𝓝[s] a)
    (hv : v ∈ 𝓝[t] b) : u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b) :=
  by
  rw [nhdsWithin_prod_eq]
  exact prod_mem_prod hu hv

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