mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'

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)

Похожие утверждения