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]