English
The differentiability of a section in total space is equivalent to the combination of base-space differentiability and fiber-differentiability in the fiber direction under a fixed trivialization.
Русский
Дифференциируемость секции в полном пространстве эквивалентна сочетанию дифференциируемости по основанию и дифференциируемости по направлению волокна в фиксированной тривиализации.
LaTeX
$$$\displaystyle MDifferentiableWithinAt IM IB f s x \iff (MDifferentiableWithinAt IM IB (fun y => (f y).proj) s x \land MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun 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. -/
theorem mdifferentiableAt_section_iff (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B))
[MemTrivializationAtlas e] (s : Π b : B, E b) {b₀ : B} (hex₀ : b₀ ∈ e.baseSet) :
MDifferentiableAt IB (IB.prod 𝓘(𝕜, F)) (fun b ↦ TotalSpace.mk' F b (s b)) b₀ ↔
MDifferentiableAt IB 𝓘(𝕜, F) (fun x ↦ (e (s x)).2) b₀ :=
by simpa [← mdifferentiableWithinAt_univ] using e.mdifferentiableWithinAt_section_iff IB s hex₀
