English
If a section is differentiable on a set, then the same section viewed in a different trivialization remains differentiable on that set provided the base point lies in the base sets.
Русский
Если секция дифференцируемa на множестве, то в другой тривиализации секция сохраняет дифференцируемость на том же множестве при условии попадания в базовые множества.
LaTeX
$$$\displaystyle MDifferentiableOn IM IB (fun x => TotalSpace.mk' F x (s x)) s x \Rightarrow MDifferentiableOn IM 𝓘(𝕜, F) (fun x => (e' (f x)).2) s x.$$$
Lean4
/-- Characterization of differentiable functions into a vector bundle in terms
of any trivialization. Version at a point. -/
theorem mdifferentiableAt_totalSpace_iff (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B))
[MemTrivializationAtlas e] (f : M → TotalSpace F E) {x₀ : M} (he : f x₀ ∈ e.source) :
MDifferentiableAt IM (IB.prod 𝓘(𝕜, F)) f x₀ ↔
MDifferentiableAt IM IB (fun x => (f x).proj) x₀ ∧ MDifferentiableAt IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) x₀ :=
by
rw [mdifferentiableAt_totalSpace]
apply and_congr_right
intro hf
rw [Trivialization.mdifferentiableAt_snd_comp_iff₂ IB (FiberBundle.mem_trivializationAt_proj_source) he hf]
