English
The tangent coordinate change is defined as the derivative of the coordinate-change map between two charts.
Русский
Переход касательных координат определён как производная перехода координат между двумя диаграммами.
LaTeX
$$$$ \mathrm{tangentCoordChange} I x y z = fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) $$$$
Lean4
/-- In a manifold `M`, given two preferred charts indexed by `x y : M`, `tangentCoordChange I x y`
is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values
outside the intersection of the sources of the two charts.
Note that this definition takes advantage of the fact that `tangentBundleCore` has the same base
sets as the preferred charts of the base manifold. -/
abbrev tangentCoordChange (x y : M) : M → E →L[𝕜] E :=
(tangentBundleCore I M).coordChange (achart H x) (achart H y)
