extend_image_nhds_mem_nhds_of_boundaryless

English

The image of a nearby set under the extended chart is near the image point.

Русский

Образ близкой множества под расширенным чартом близок к образу точки.

LaTeX

$$$ (f^{\\mathrm{extend}}_I)[s] \\in \\mathcal{N}((f^{\\mathrm{extend}}_I)(x)) \\quad \\text{for } s \\ni x, \\ x \\in f.source. $$$

Lean4

theorem extend_image_nhds_mem_nhds_of_boundaryless [I.Boundaryless] {x} (hx : x ∈ f.source) {s : Set M} (h : s ∈ 𝓝 x) :
    (f.extend I) '' s ∈ 𝓝 ((f.extend I) x) :=
  by
  rw [← f.map_extend_nhds_of_boundaryless hx, Filter.mem_map]
  filter_upwards [h] using subset_preimage_image (f.extend I) s

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