English
Around a point in the target, extChartAt I x .target and range I coincide locally.
Русский
В окрестности точки в target множество extChartAt I x .target и range I совпадают локально.
LaTeX
$$$ extChartAt I x . target =^\\mathcal{N}_{(extChartAt I x).toFun y} range I \\quad (y\\in (extChartAt I x).source) $$$
Lean4
/-- Around the image of a point in the source, `(extChartAt I x).target` and `range I`
coincide locally. -/
theorem extChartAt_target_eventuallyEq' {x y : M} (hy : y ∈ (extChartAt I x).source) :
(extChartAt I x).target =ᶠ[𝓝 (extChartAt I x y)] range I :=
nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq' hy)