comap_nhds_eq — Mathlib

English

Equality of comap and nhdsSet under closed map and continuous assumptions.

Русский

Равенство comap и nhdsSet при замкнутом отображении и непрерывности.

LaTeX

$$$IsClosedMap f \\land Continuous f \\rightarrow comap f (\\mathcal{N} y) = \\mathcal{N}_{Y}^s (f^{-1}\\{y\\})$$$

Lean4

theorem comap_nhds_eq (hf : IsClosedMap f) (hf' : Continuous f) (y : Y) : comap f (𝓝 y) = 𝓝ˢ (f ⁻¹' { y }) :=
  le_antisymm
    (isClosedMap_iff_comap_nhds_le.mp hf)
      -- Note: below should be an application of `Continuous.tendsto_nhdsSet_nhds`, but this is only
        -- proven later...

    (nhdsSet_le.mpr fun x hx ↦ hx ▸ (hf'.tendsto x).le_comap)

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