nhds_def — Mathlib

English

For x in tsze R M, the neighborhood filter equals the product of the neighborhood filters of the first and second components.

Русский

Для x в tsze R M окрестностная фильтра равна произведению окрестностных фильтров x.fst и x.snd.

LaTeX

$$$\\mathcal{N}_{tsze(R,M)}(x)=\\mathcal{N}_{R}(x.fst)\\times\\mathcal{N}_{M}(x.snd).$$$

Lean4

theorem nhds_def (x : tsze R M) : 𝓝 x = 𝓝 x.fst ×ˢ 𝓝 x.snd :=
  nhds_prod_eq

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