English
If x ∈ f.source and f.extend I x lies in interior(range I), then the image of any neighborhood s of x under the extension is a neighborhood of (f.extend I)x.
Русский
Если x ∈ f.source и f.extend I x лежит во внутренности диапазона, то образ любой окрестности s(x) под расширением является окрестностью точки (f.extend I)x.
LaTeX
$$$ x \\in f.source \\land f^{\\mathrm{extend}}_I x \\in \\mathrm{Int}(\\mathrm{range}(I)) \\Rightarrow (f^{\\mathrm{extend}}_I)[s] \\in \\mathcal{N}((f^{\\mathrm{extend}}_I)(x)). $$$
Lean4
theorem extend_image_nhds_mem_nhds_of_mem_interior_range {x} (hx : x ∈ f.source)
(h'x : f.extend I x ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 x) : (f.extend I) '' s ∈ 𝓝 ((f.extend I) x) :=
by
rw [← f.map_extend_nhds_of_mem_interior_range hx h'x, Filter.mem_map]
filter_upwards [h] using subset_preimage_image (f.extend I) s