English
Around a point in the target, the neighborhoods of extChartAt I x y inside the target equal those inside range I.
Русский
В окрестности точки в целевом диапазоне окрестности extChartAt I x y внутри target равны окрестностям внутри range I.
LaTeX
$$$\\forall x,y:(\\text{hy}): \\, \\mathcal{N}_{(extChartAt I x).target}(extChartAt I x y) = \\mathcal{N}_{\\mathrm{range} I}(extChartAt I x y).$$$
Lean4
/-- Around the image of a point in the source, the neighborhoods are the same
within `(extChartAt I x).target` and within `range I`. -/
theorem nhdsWithin_extChartAt_target_eq' {x y : M} (hy : y ∈ (extChartAt I x).source) :
𝓝[(extChartAt I x).target] extChartAt I x y = 𝓝[range I] extChartAt I x y :=
nhdsWithin_extend_target_eq _ <| by rwa [← extChartAt_source I]