English
For each x, the trivialization at x matches the local trivialization arising from tangentBundleCore.
Русский
Для каждой точки x тривиализация в точке x совпадает с локальной тривиализацией, полученной из tangentBundleCore.
LaTeX
$$$$ \operatorname{trivializationAt} E (\mathrm{TangentSpace} I) x = (\mathrm{tangentBundleCore} I M).toFiberBundleCore.localTriv (\mathrm{achart} H x) $$$$
Lean4
theorem chartAt_toPartialEquiv (p : TM) :
(chartAt (ModelProd H E) p).toPartialEquiv =
(tangentBundleCore I M).toFiberBundleCore.localTrivAsPartialEquiv (achart H p.1) ≫
(chartAt H p.1).toPartialEquiv.prod (PartialEquiv.refl E) :=
rfl