English
The extension map extChartAt acts as the extended chart obtained by precomposing with the model with corners I; in particular, its underlying function coincides with the composition of I with the standard chart at.
Русский
Расширенная карта extChartAt получается как продолжение карты, полученной через предобраз с моделью corners I; её функция равна композиции I с обычной картой в точке.
LaTeX
$$$\\mathrm{extChartAt}(I,x) = (I) \\circ (\\mathrm{chartAt}\\,H\\,x)$$$
Lean4
/-- The preferred extended chart on a manifold with corners around a point `x`, from a neighborhood
of `x` to the model vector space. -/
@[simp, mfld_simps]
def extChartAt (x : M) : PartialEquiv M E :=
(chartAt H x).extend I
