extChartAt_image_nhds_mem_nhds_of_mem_interior_range

English

If y is in the source and extChartAt I x y lies in the interior of range I, then for any s ∈ 𝓝 y, the image extChartAt I x '' s is in 𝓝 (extChartAt I x y).

Русский

Если y в source и extChartAt I x y лежит во внутренности range I, то для любого s ∈ 𝓝 y образ extChartAt I x '' s принадлежит 𝓝 (extChartAt I x y).

LaTeX

$$$\\mathrm{hy}: y \\in (\\mathrm{extChartAt} I x).\\mathrm{source} \\land h'\\!:\\ extChartAt I x y \\in \\mathrm{interior}(\\mathrm{range} I) \\Rightarrow \\forall s, \\ s \\in \\mathcal{N}(y) \\Rightarrow (\\mathrm{extChartAt} I x)''s \\in \\mathcal{N}(\\mathrm{extChartAt} I x y) $$$

Lean4

theorem extChartAt_image_nhds_mem_nhds_of_mem_interior_range {x y} (hx : y ∈ (extChartAt I x).source)
    (h'x : extChartAt I x y ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 y) :
    (extChartAt I x) '' s ∈ 𝓝 (extChartAt I x y) := by
  rw [extChartAt]
  exact extend_image_nhds_mem_nhds_of_mem_interior_range _ (by simpa using hx) h'x h

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