image_mem_nhds — Mathlib

English

For an open map f, the image of a neighborhood of x is a neighborhood of f(x).

Русский

Для открытого отображения f образ окрестности точки x является окрестностью f(x).

LaTeX

$$$$IsOpenMap(f) \\rightarrow \\forall x \\in X, \\forall s \\ni x, f''s \\in \\mathcal{N}(f(x))$$$$

Lean4

theorem image_mem_nhds (hf : IsOpenMap f) {x : X} {s : Set X} (hx : s ∈ 𝓝 x) : f '' s ∈ 𝓝 (f x) :=
  let ⟨t, hts, ht, hxt⟩ := mem_nhds_iff.1 hx
  mem_of_superset (IsOpen.mem_nhds (hf t ht) (mem_image_of_mem _ hxt)) (image_mono hts)

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