English
For a trivialization, differentiability of the total-space projection coincides with differentiability of the fiber component after switching to the other trivialization at a fixed point.
Русский
Для тривиализации дифференцируемость проекции полного пространства совпадает с дифференцируемостью компоненты волокна после смены тривиализации в фиксированной точке.
LaTeX
$$$\displaystyle MDifferentiableAt IM 𝓘(𝕜, F) (\lambda x. (e (f x)).2) x \iff MDifferentiableAt IM 𝓘(𝕜, F) (\lambda x. (e' (f x)).2) x.$$$
Lean4
/-- Characterization of differentiable functions into a vector bundle in terms
of any trivialization. Version at a point within at set. -/
theorem mdifferentiableWithinAt_section_iff (e : Trivialization F (TotalSpace.proj : TotalSpace F E → B))
[MemTrivializationAtlas e] (s : Π b : B, E b) {u : Set B} {b₀ : B} (hex₀ : b₀ ∈ e.baseSet) :
MDifferentiableWithinAt IB (IB.prod 𝓘(𝕜, F)) (fun b ↦ TotalSpace.mk' F b (s b)) u b₀ ↔
MDifferentiableWithinAt IB 𝓘(𝕜, F) (fun x ↦ (e (s x)).2) u b₀ :=
by
rw [e.mdifferentiableWithinAt_totalSpace_iff IB]
· change MDifferentiableWithinAt IB IB id u b₀ ∧ _ ↔ _
simp [mdifferentiableWithinAt_id]
exact (coe_mem_source e).mpr hex₀
