English
The chart at a tangent bundle point is a composition of the fondamental trivialization with the base chart, as described by the main formula.
Русский
Чарта касательного расслоения в точке задаётся как композиция тривиализации и базовой диаграммы, согласно основной формуле.
LaTeX
$$$$ \mathrm{chartAt}(\mathrm{ModelProd} H E) p = ((\mathrm{tangentBundleCore} I M).toFiberBundleCore.localTriv (\mathrm{achart} H p.1)).toOpenPartialHomeomorph \circ (\mathrm{chartAt} H p.1).prod (\mathrm{OpenPartialHomeomorph.refl} E) $$$$
Lean4
protected theorem chartAt (p : TM) :
chartAt (ModelProd H E) p =
((tangentBundleCore I M).toFiberBundleCore.localTriv (achart H p.1)).toOpenPartialHomeomorph ≫ₕ
(chartAt H p.1).prod (OpenPartialHomeomorph.refl E) :=
rfl
