English
Let I be a ModelWithCorners and x ∈ M. The inverse of the extended chart at x induces a homeomorphism between a neighborhood of extChartAt I x x within the chart's range and a neighborhood of x in M; equivalently, the inverse chart maps a neighborhood in the chart image back to a neighborhood of x, preserving local topological structure.
Русский
Пусть I задаёт модель с углами и x ∈ M. Обратная карта расширенной шкалы в точке x устанавливает гомеоморфизм между окрестностью extChartAt I x x внутри области определения карты и окрестностью x в M; другими словами, обратная карта отображает окрестность в образе карты обратно в окрестность x, сохраняя локальную топологическую структуру.
LaTeX
$$$\operatorname{map}((\mathrm{extChartAt} I x)^{-1}, \mathcal{N}_{\mathrm{range}(I)}(\mathrm{extChartAt} I x x)) = \mathcal{N}(x).$$$
Lean4
theorem map_extChartAt_symm_nhdsWithin_range (x : M) : map (extChartAt I x).symm (𝓝[range I] extChartAt I x x) = 𝓝 x :=
map_extChartAt_symm_nhdsWithin_range' (mem_extChartAt_source x)
