English
Equivalence of differentiability of a section in total space with the pair of base projection differentiability and fiber coordinate differentiability under a given trivialization.
Русский
Эквивалентность дифференцируемости секции в полном пространстве и пары дифференцируемости проекции на основание и координат волокна в рамках тривиализации.
LaTeX
$$$\displaystyle MDifferentiableWithinAt IM IB f s x \iff MDifferentiableWithinAt IM IB (f \mapsto f.x) s x \land MDifferentiableWithinAt IM 𝓘(𝕜, F) (\lambda y. (e (f y)).2) s x.$$$
Lean4
/-- Characterization of differentiable functions into a vector bundle in terms
of any trivialization. Version at a point within at set. -/
theorem mdifferentiableWithinAt_totalSpace_iff (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B))
[MemTrivializationAtlas e] (f : M → TotalSpace F E) {s : Set M} {x₀ : M} (he : f x₀ ∈ e.source) :
MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F)) f s x₀ ↔
MDifferentiableWithinAt IM IB (fun x => (f x).proj) s x₀ ∧
MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) s x₀ :=
by
rw [mdifferentiableWithinAt_totalSpace]
apply and_congr_right
intro hf
rw [Trivialization.mdifferentiableWithinAt_snd_comp_iff₂ IB (FiberBundle.mem_trivializationAt_proj_source) he hf]
