extChartAt_target_mem_nhds — Mathlib

English

If I is boundaryless, then the target of the extended chart at x is a neighborhood of the point extChartAt I x x.

Русский

Пусть I не имеет границы (boundaryless). Тогда множество target расширенного графа в точке x является окрестностью точки extChartAt I x x.

LaTeX

$$$ (extChartAt I x).target \\in \\mathcal{N}((extChartAt I x) x) $$$

Lean4

/-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of the key point -/
theorem extChartAt_target_mem_nhds [I.Boundaryless] (x : M) : (extChartAt I x).target ∈ 𝓝 (extChartAt I x x) :=
  by
  convert extChartAt_target_mem_nhdsWithin x
  simp only [I.range_eq_univ, nhdsWithin_univ]

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