English
Let f: M → TotalSpace F E be differentiable at x in the sense of the total space; then f is MDifferentiable at x iff its projection is MDifferentiable and its fiber coordinate is differentiable at x.
Русский
Пусть f: M → TotalSpace F E дифференцируема в точке x; тогда дифференцируемость f в точке эквивалентна дифференцируемости проекции и проекции волокна в x.
LaTeX
$$$$MDifferentiableAt IM (IB.prod 𝓘(\mathbb{k}, F)) f x \iff \Big( MDifferentiableAt IM IB (\lambda x: f(x).proj) x \wedge MDifferentiableAt IM 𝓘(\mathbb{k}, F) (\lambda x: (\\text{trivializationAt } F E (f x_0).proj (f x)).2) x \Big).$$$$
Lean4
/-- Characterization of differentiable functions into a vector bundle.
Version at a point -/
theorem mdifferentiableAt_totalSpace (f : M → TotalSpace F E) {x₀ : M} :
MDifferentiableAt IM (IB.prod 𝓘(𝕜, F)) f x₀ ↔
MDifferentiableAt IM IB (fun x => (f x).proj) x₀ ∧
MDifferentiableAt IM 𝓘(𝕜, F) (fun x ↦ (trivializationAt F E (f x₀).proj (f x)).2) x₀ :=
by simpa [← mdifferentiableWithinAt_univ] using mdifferentiableWithinAt_totalSpace _ f
