mfderiv_chartAt_eq_tangentCoordChange

English

The derivative in chart coordinates between two charts equals the tangent coordinate change map.

Русский

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

LaTeX

$$$mfderiv\\ I\\ I'\\ (chartAt\\ H\\ y)\\ x = tangentCoordChange\\ I x y x$$$

Lean4

theorem mfderiv_chartAt_eq_tangentCoordChange {x y : M} (hsrc : x ∈ (chartAt H y).source) :
    mfderiv I I (chartAt H y) x = tangentCoordChange I x y x :=
  by
  have := mdifferentiableAt_atlas (I := I) (ChartedSpace.chart_mem_atlas _) hsrc
  simp [mfderiv, if_pos this, Function.comp_assoc]

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