tangentBundleCore_coordChange_achart

English

The tangent coordinate change equals the derivative of the extChartAt map between x and y, at z.

Русский

Переход касательных координат равен производной extChartAt между x и y в точке z.

LaTeX

$$$$ \mathrm{tangentCoordChange} I x y z = fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) $$$$

Lean4

theorem tangentBundleCore_coordChange_achart (x x' z : M) :
    (tangentBundleCore I M).coordChange (achart H x) (achart H x') z =
      fderivWithin 𝕜 (extChartAt I x' ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) :=
  rfl

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