English
There is a natural equality expressing extChartAt in terms of trivialization and base chart data, i.e., the chart on the total space is the combination of base and fiber charts.
Русский
Существует естественное равенство extChartAt в терминах тривиализации и данных базовой чарты: чарта на общем пространстве является сочетанием базовой и волоконной чарты.
LaTeX
$$$$ extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x = (trivializationAt F E x.proj).toPartialEquiv \\circ (extChartAt IB x.proj).prod (PartialEquiv.refl F). $$$$
Lean4
protected theorem extChartAt_target (x : TotalSpace F E) :
(extChartAt (IB.prod 𝓘(𝕜, F)) x).target =
((extChartAt IB x.proj).target ∩ (extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ :=
by
rw [FiberBundle.extChartAt, PartialEquiv.trans_target, Trivialization.target_eq, inter_prod]
rfl
