isInvertible_mfderivWithin_extChartAt_symm

English

Again, mfderivWithin extChartAt_symm is invertible at y.

Русский

Снова mfderivWithin extChartAt_symm обратимо в точке y.

LaTeX

$$$(mfderivWithin 𝓘(𝕜,E) I (extChartAt I x).symm (range I) y).IsInvertible$$$

Lean4

theorem isInvertible_mfderivWithin_extChartAt_symm {y : E} (hy : y ∈ (extChartAt I x).target) :
    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y).IsInvertible :=
  ContinuousLinearMap.IsInvertible.of_inverse (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt hy)
    (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm hy)

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