English
Let f be a map from a manifold M into the total space of a vector bundle E over B. Then f is C^n with respect to the product model on the total space if and only if its base projection is C^n and the fibre-coordinate in a local trivialization is C^n at the base point x0. In other words, differentiability of a map into the total space decomposes into differentiability of the base map and differentiability of the local fibre coordinate.
Русский
Пусть f: M → общее пространство векторного расслоения E над B. Тогда f является C^n в точке x0 относительно произведенной структуры пространства, если и только если проекция на основание является C^n, и координаты волокна в локальной тривиализации тоже C^n в точке основания.
LaTeX
$$$\displaystyle \text{ContMDiffAt } IM \,(IB. prod\, 𝓘(\mathit{𝕜}, F))\, n\, f\, x_0 \;\longleftrightarrow\; (\text{ContMDiffAt } IM\, IB\, n\, (\lambda x. f(x).proj)\, x_0)\; \land\; (\text{ContMDiffAt } IM\, 𝓘(\mathit{𝕜}, F)\, n\, (\lambda x. (\text{trivializationAt } F E (f x_0).proj (f x)).2)\, x_0).$$$
Lean4
/-- Characterization of `C^n` functions into a vector bundle. Version at a point. -/
theorem contMDiffAt_totalSpace {f : M → TotalSpace F E} {x₀ : M} :
ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔
ContMDiffAt IM IB n (fun x ↦ (f x).proj) x₀ ∧
ContMDiffAt IM 𝓘(𝕜, F) n (fun x ↦ (trivializationAt F E (f x₀).proj (f x)).2) x₀ :=
by simp_rw [← contMDiffWithinAt_univ]; exact contMDiffWithinAt_totalSpace
