English
If hb is in the source of chartOn H b0, then the continuous linear map at the trivialization equals the core coordinate change, i.e., trivializationAt-continuousLinearMapAt equals tangentBundleCore.coordChange.
Русский
Если hb принадлежит области определения чарта в b0, то непрерывно-линейное отображение тривиализации равно координатному изменению ядра касательного пространства.
LaTeX
$$$\mathrm{trivializationAt}\,E\,(\mathrm{TangentSpace}\,I)\;b_0\,\mathrm{continuousLinearMapAt}\;\mathbb{K}\;b = (\mathrm{tangentBundleCore}\;I\;M).coordChange (\operatorname{achart} H b) (\operatorname{achart} H b_0) b$$$
Lean4
/-- The trivialization of the tangent space can be expressed in terms of the tangent bundle core.
To write it as the manifold derivative of `extChartAt`, see
`TangentBundle.continuousLinearMapAt_trivializationAt`.
Use with care as it abuses the defeq `TangentSpace I b = E`. -/
theorem continuousLinearMapAt_trivializationAt_eq_core {b₀ b : M} (hb : b ∈ (chartAt H b₀).source) :
(trivializationAt E (TangentSpace I) b₀).continuousLinearMapAt 𝕜 b =
(tangentBundleCore I M).coordChange (achart H b) (achart H b₀) b :=
by simp [hb]
