English
A pointwise C^n version: if hψ, hv, hw hold at x, then the bilinear application ψ m (v m) (w m) is C^n differentiable at x.
Русский
Точечно-точечная версия C^n: если hψ, hv, hw в точке x, тогда билинейное применение ψ m (v m) (w m) дифференцируемо до порядка C^n в x.
LaTeX
$$$$\text{ContMDiffAt IM (IB. prod 𝓘(\mathbb{k}, F_1 \to_L F_2 \to_L F_3)) n (m \mapsto \mathrm{TotalSpace.mk}' F_3 (b m) (\psi m (v m) (w m)))} x.$$$$
Lean4
/-- Characterization of differentiable sections of a vector bundle at a point within a set
in terms of the preferred trivialization at that point. -/
theorem mdifferentiableAt_section (s : Π b, E b) {b₀ : B} :
MDifferentiableAt IB (IB.prod 𝓘(𝕜, F)) (fun b ↦ TotalSpace.mk' F b (s b)) b₀ ↔
MDifferentiableAt IB 𝓘(𝕜, F) (fun b ↦ (trivializationAt F E b₀ (s b)).2) b₀ :=
by simpa [← mdifferentiableWithinAt_univ] using mdifferentiableWithinAt_section _ _
