English
For a trivialization, the differentiability of the total-space projection composed with a section is equivalent to the differentiability of the coordinates in the fiber after projecting to the base and then comparing with another trivialization.
Русский
Для тривиализации дифференциация составного отображения секции и проекции равна дифференцируемости координат внутри сосудов после проекции на основание и сравнения с другой тривиализацией.
LaTeX
$$$\displaystyle MDifferentiableWithinAt IM IB (\pi F E \circ f) s x \Rightarrow (\text{iff})\ MDifferentiableWithinAt IM 𝓘(𝕜, F) (\lambda x. (e (f x)).2) s x.$$$
Lean4
theorem mdifferentiableAt_snd_comp_iff₂ {e e' : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e]
[MemTrivializationAtlas e'] {f : M → TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) (he' : f x₀ ∈ e'.source)
(hf : MDifferentiableAt IM IB (fun x ↦ (f x).proj) x₀) :
MDifferentiableAt IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) x₀ ↔ MDifferentiableAt IM 𝓘(𝕜, F) (fun x ↦ (e' (f x)).2) x₀ := by
simpa [← mdifferentiableWithinAt_univ] using e.mdifferentiableWithinAt_snd_comp_iff₂ IB he he' hf
