English
Another repetition: MDifferentiableOn for extChartAt symm target.
Русский
Ещё одно повторение: MDifferentiableOn для extChartAt symm.
LaTeX
$$$\mathrm{MDifferentiableOn}\;\bigl(\mathrm{modelWithCornersSelf} \; \; I\bigr) \; I \; (\mathrm{extChartAt} I x).symm.toFun$$
Lean4
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).source`. -/
theorem mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' {y : M} (hy : y ∈ (extChartAt I x).source) :
(mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (extChartAt I x y)) ∘L
(mfderiv I 𝓘(𝕜, E) (extChartAt I x) y) =
ContinuousLinearMap.id _ _ :=
by
have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
convert mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)