extChartAt_image_nhds_mem_nhds_of_boundaryless

English

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

Русский

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

LaTeX

$$$extChartAt I x '' s \\in 𝓝 (extChartAt I x y)$$$

Lean4

theorem extChartAt_image_nhds_mem_nhds_of_boundaryless [I.Boundaryless] {x : M} (hx : s ∈ 𝓝 x) :
    extChartAt I x '' s ∈ 𝓝 (extChartAt I x x) := by
  rw [extChartAt]
  exact extend_image_nhds_mem_nhds_of_boundaryless _ (mem_chart_source H x) hx

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