English
If z lies in the intersection of the chart sources, then the derivative of the coordinate change is described by HasFDerivWithinAt for the appropriate map.
Русский
Если z принадлежит пересечению областей источников диаграмм, то производная перехода координат описывается через HasFDerivWithinAt для соответствующей отображения.
LaTeX
$$$$ HasFDerivWithinAt\big((\mathrm{extChartAt} I y) \circ (\mathrm{extChartAt} I x).symm\big)\big( \mathrm{tangentCoordChange} I x y z \big)\big( \mathrm{range} I \big)\big(\mathrm{extChartAt} I x z\big). $$$$
Lean4
theorem tangentCoordChange_def {x y z : M} :
tangentCoordChange I x y z = fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) :=
rfl