English
The coordChange field of tangentBundleCore with charts x,y is the derivative of the coordinate change map between extChartAt I x and extChartAt I y.
Русский
Поле coordChange у tangentBundleCore для диаграмм x,y равно производной перехода координат между extChartAt I x и extChartAt I y.
LaTeX
$$$$ (tangentBundleCore I M).coordChange (\mathrm{achart} H x) (\mathrm{achart} H y) z = fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z). $$$$
Lean4
/-- `simp`-normal form is `tangentBundleCore_localTriv_baseSet`. -/
theorem tangentBundleCore_baseSet (i) : (tangentBundleCore I M).baseSet i = i.1.source :=
rfl