mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm'

English

Same as earlier composition identity for extChartAt and its symm under mfderiv.

Русский

Повтор того же соотношения композиции производных для extChartAt и его симметричной карты.

LaTeX

$$$ mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm \\ (вариант) $$$

Lean4

/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).source`. -/
theorem mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm' {x : M} {y : M} (hy : y ∈ (extChartAt I x).source) :
    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y) ∘L
        (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (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 mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm ((extChartAt I x).map_source hy)

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