English
The value of the tangent bundle trivialization at x on a tangent vector z is given by the pair consisting of the base point z.1 and the derivative component along a specified chart composition.
Русский
Значение тривиализации касательного пространства в точке x на касательном векторе z равно паре, состоящей из базовой точки z.1 и производной второй компоненты вдоль заданного композиционного чарта.
LaTeX
$$$\mathrm{trivializationAt}\,E\,(\mathrm{TangentSpace}\,I)\,x\,z = \Bigl(z.1,\; fderivWithin\,\mathbb{k}\Bigl( (chartAt\;H\;x) \circ (\text{extend}\;I) \circ \bigl( (chartAt\;H\;z.1) \circ \text{extend}\;I \bigr)^{-1} \Bigr)\!\!(\text{range }I)\,z.2 \Bigr)$$$$
Lean4
theorem trivializationAt_apply (x : M) (z : TM) :
trivializationAt E (TangentSpace I) x z =
(z.1,
fderivWithin 𝕜 ((chartAt H x).extend I ∘ ((chartAt H z.1).extend I).symm) (range I)
((chartAt H z.1).extend I z.1) z.2) :=
rfl
