trivializationAt_eq_localTriv — Mathlib

English

The source of the tangent bundle trivialization equals the preimage under the projection of the chart source.

Русский

Область определения тривиализации касательного расслоения равна предобразованию по проекции от источника диаграммы.

LaTeX

$$$$ (\operatorname{trivializationAt} E (\mathrm{TangentSpace} I) x).\mathrm{source} = \pi E(\mathrm{TangentSpace} I)^{-1} (\mathrm{chartAt} H x).\mathrm{source} $$$$

Lean4

theorem trivializationAt_eq_localTriv (x : M) :
    trivializationAt E (TangentSpace I) x = (tangentBundleCore I M).toFiberBundleCore.localTriv (achart H x) :=
  rfl

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