English
Equality of inTangentCoordinates: the coordinate change map equals the direct mapping in model-space coordinates.
Русский
Равенство inTangentCoordinates: отображение смены координат совпадает с прямым отображением в координатах модельного пространства.
LaTeX
$$$inTangentCoordinates I I' f g ϕ x_0 x = ϕ$$$
Lean4
/-- To write a linear map between tangent spaces in coordinates amounts to precomposing and
postcomposing it with suitable coordinate changes. For a concrete version expressing the
change of coordinates as derivatives of extended charts,
see `inTangentCoordinates_eq_mfderiv_comp`. -/
theorem inTangentCoordinates_eq (f : N → M) (g : N → M') (ϕ : N → E →L[𝕜] E') {x₀ x : N}
(hx : f x ∈ (chartAt H (f x₀)).source) (hy : g x ∈ (chartAt H' (g x₀)).source) :
inTangentCoordinates I I' f g ϕ x₀ x =
(tangentBundleCore I' M').coordChange (achart H' (g x)) (achart H' (g x₀)) (g x) ∘L
ϕ x ∘L (tangentBundleCore I M).coordChange (achart H (f x₀)) (achart H (f x)) (f x) :=
(tangentBundleCore I M).inCoordinates_eq (tangentBundleCore I' M') (ϕ x) hx hy
