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)