chartAt_toPartialEquiv — Mathlib

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

Похожие утверждения