English
Let s: B → E x be a section. The map x ↦ TotalSpace.mk' F x (s x) is C^n at x0 if and only if the base projection to B composed with the trivialization coordinate at x0 is C^n at x0. This provides a pointwise criterion for differentiability of a section via a local trivialization.
Русский
Пусть s: B → E x — секция. Отображение x ↦ TotalSpace.mk' F x (s x) является C^n в точке x0 тогда и только тогда, когда базовая проекция в сочетании с координатами тривиализации в точке x0 является C^n в x0.
LaTeX
$$$\displaystyle \operatorname{ContMDiffAt} IB (IB. prod 𝓘(\mathit{𝕜}, F))\; n\; (\\lambda x, TotalSpace.mk' F x (s x))\ x_0 \\ \Longleftrightarrow\\ \operatorname{ContMDiffAt} IB 𝓘(\mathit{𝕜}, F)\; n\; (\\lambda x, (trivializationAt F E x_0 ⟨x, s x⟩).2)\ x_0.$$$
Lean4
/-- Characterization of `C^n` sections of a vector bundle. -/
theorem contMDiffAt_section {s : ∀ x, E x} (x₀ : B) :
ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x₀ ↔
ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (trivializationAt F E x₀ ⟨x, s x⟩).2) x₀ :=
by simp_rw [contMDiffAt_totalSpace, and_iff_right_iff_imp]; intro; exact contMDiffAt_id
