nhds_coe_eq — Mathlib

English

For every x in X, the neighborhood filter at the image of x in the one-point compactification equals the pushforward of the neighborhood filter at x along the natural embedding X → OnePoint X.

Русский

Для каждого x из X множество окрестностей точки x в OnePoint X совпадает с отображением фильтра окрестностей x через включение X → OnePoint X.

LaTeX

$$$\mathcal{N}(\iota x) = \operatorname{map}(\iota)(\mathcal{N}x),$ where $\iota: X \hookrightarrow \operatorname{OnePoint} X$ is the natural embedding.$$

Lean4

theorem nhds_coe_eq (x : X) : 𝓝 ↑x = map ((↑) : X → OnePoint X) (𝓝 x) :=
  (isOpenEmbedding_coe.map_nhds_eq x).symm

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