English
Coordinate changes compose: applying consecutive tangent coordinate changes yields the direct tangent coordinate change between the outer charts.
Русский
Переходы координат компонуются: применение последовательных переходов касательных координат даёт переход между внешними диаграммами.
LaTeX
$$$$ (\mathrm{tangentCoordChange} I x y z) \circ (\mathrm{tangentCoordChange} I w x z) = \mathrm{tangentCoordChange} I w y z $$$$
Lean4
theorem tangentCoordChange_comp {w x y z : M} {v : E}
(h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source) :
tangentCoordChange I x y z (tangentCoordChange I w x z v) = tangentCoordChange I w y z v :=
by
apply (tangentBundleCore I M).coordChange_comp
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]
exact h
