comap_coe_nhds — Mathlib

English

The comap of nhds at ∞ along the inclusion X → OnePoint X equals nhds at ∞ in OnePoint X.

Русский

Обратное изображение фильтра окрестностей ∞ через вложение X → OnePoint X совпадает с nhds на ∞ в OnePoint X.

LaTeX

$$$\operatorname{comap}(\iota)(\mathcal{N}x) = \mathcal{N}x$ for $x$ in $X$, i.e. $\operatorname{comap}(\iota)(\mathcal{N}(\iota x)) = \mathcal{N}(x)$.$$

Lean4

theorem comap_coe_nhds (x : X) : comap ((↑) : X → OnePoint X) (𝓝 x) = 𝓝 x :=
  (isOpenEmbedding_coe.isInducing.nhds_eq_comap x).symm

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