comap_nhdsSet_eq — Mathlib

English

Equivalent formulation of comap-nhdsSet equality for all s.

Русский

Эквивалентная формулировка равенства comap-nhdsSet для всех s.

LaTeX

$$$IsClosedMap f \\land Continuous f \\rightarrow \\forall s, comap f (\\mathcal{N}^s s) = \\mathcal{N}^s (f^{-1}s)$$$

Lean4

theorem comap_nhdsSet_eq (hf : IsClosedMap f) (hf' : Continuous f) (s : Set Y) : comap f (𝓝ˢ s) = 𝓝ˢ (f ⁻¹' s) :=
  le_antisymm
    (isClosedMap_iff_comap_nhdsSet_le.mp hf)
      -- Note: below should be an application of `Continuous.tendsto_nhdsSet_nhdsSet`, but this is only
        -- proven later...

    (nhdsSet_le.mpr fun x hx ↦ (hf'.tendsto x).le_comap.trans (comap_mono (nhds_le_nhdsSet hx)))

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