English
Let f: M → LE1E2 be a bundle morphism. Differentiability of f at a point x0 in the product decomposition is equivalent to differentiability of its base component and the induced coordinates component inCoordinates at x0.
Русский
Пусть f: M → LE1E2 – отображение между пакетами; дифференцируемость f в точке x0 равносильна дифференцируемости базовой части и координатной части вCoordinates в x0.
LaTeX
$$$\\text{mdiffAt}(f,x_0) \\iff \\text{mdiffAt}(f|_\\text{base},x_0) \\land \\text{mdiffAt}(\\text{inCoordinates}(f,x_0),x_0)$$$
Lean4
theorem hom_chart (y₀ y : LE₁E₂) :
chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀ y =
(chartAt HB y₀.1 y.1, inCoordinates F₁ E₁ F₂ E₂ y₀.1 y.1 y₀.1 y.1 y.2) :=
by
rw [FiberBundle.chartedSpace_chartAt, trans_apply, OpenPartialHomeomorph.prod_apply, Trivialization.coe_coe,
OpenPartialHomeomorph.refl_apply, Function.id_def, hom_trivializationAt_apply]
