extend_image_nhds_mem_nhds_of_mem_interior_range

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

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