nhds_prod_eq — Mathlib

English

The neighborhood filter at (x,y) on the product X × Y is the product of neighborhood filters: nhds(x,y) = nhds(x) × nhds(y).

Русский

Гуверниндж-фильтр в точке (x,y) на произведении равен произведению фильтров окрестностей: nhds(x,y) = nhds(x) × nhds(y).

LaTeX

$$$\ nhds (x,y) = (\ nhds x) \times (\ nhds y)$$$

Lean4

theorem nhds_prod_eq {x : X} {y : Y} : 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y := by
  rw [prod_eq_inf, instTopologicalSpaceProd,
    nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _) (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced,
    nhds_induced]

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