English
A total space of a fiber bundle with appropriate model with corners inherits a C^n structure from the base and fiber charts, with a concrete description of extChartAt.
Русский
Общая пространство волокна с подходящей моделью сохраняет структуру C^n на основе и волокна, с конкретным описанием extChartAt.
LaTeX
$$$$ ContMDiffWithinAt_{TotalSpace} $$$$
Lean4
protected theorem extChartAt (x : TotalSpace F E) :
extChartAt (IB.prod 𝓘(𝕜, F)) x =
(trivializationAt F E x.proj).toPartialEquiv ≫ (extChartAt IB x.proj).prod (PartialEquiv.refl F) :=
by
simp_rw [extChartAt, FiberBundle.chartedSpace_chartAt, extend]
simp only [PartialEquiv.trans_assoc, mfld_simps]
-- Porting note: should not be needed
rw [PartialEquiv.prod_trans, PartialEquiv.refl_trans]
