map_nhdsSet_eq — Mathlib

English

If f is open and continuous, then map f of nhdsSet s equals nhdsSet of f''s.

Русский

Если f открытое и непрерывное отображение, то образ nhdsSet(s) равен nhdsSet(f''s).

LaTeX

$$$$IsOpenMap(f) \\rightarrow Continuous(f) \\rightarrow \\forall s, map(f)(\\mathcal{N}\\mathcal{H}\\mathcal{D}s) = \\mathcal{N}\\mathcal{H}\\mathcal{D}(f''s)$$$$

Lean4

theorem map_nhdsSet_eq (hf : IsOpenMap f) (hf' : Continuous f) (s : Set X) : map f (𝓝ˢ s) = 𝓝ˢ (f '' s) :=
  by
  rw [← biUnion_of_singleton s]
  simp_rw [image_iUnion, nhdsSet_iUnion, map_iSup, image_singleton, nhdsSet_singleton, hf.map_nhds_eq hf'.continuousAt]

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