mdifferentiableOn_extChartAt_symm

English

The map extChartAt I x, viewed as a map from its source to its symm target, is MDifferentiable on its source.

Русский

Карта extChartAt I x, взятая как отображение из области определения в ее симметрическую цель, дифференцируема на своей области.

LaTeX

$$$\mathrm{MDifferentiableOn}\;\,\bigl(\mathrm{extChartAt} I x).symm.toFun (\mathrm{extChartAt} I x).target$$$

Lean4

theorem mdifferentiableOn_extChartAt_symm : MDifferentiableOn 𝓘(𝕜, E) I (extChartAt I x).symm (extChartAt I x).target :=
  by
  intro y hy
  exact (mdifferentiableWithinAt_extChartAt_symm hy).mono (extChartAt_target_subset_range x)

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