English
For a fixed trivialization e, differentiability of a map into the total space is equivalent to differentiability of its base-projection and of the fiber component in the chosen trivialization.
Русский
Для фиксированной тривиализации e дифференциальность отображения в полное пространство эквивалентна дифференцируемости проекции на основание и компоненты волокна в выбранной тривиализации.
LaTeX
$$$\displaystyle MDifferentiableWithinAt\! IM IB f s x \iff \ bigl( MDifferentiableWithinAt IM IB (\lambda y. (f y).proj) s x \land MDifferentiableWithinAt IM 𝓘(\mathbb{K}, F) (\lambda y. (e (f y)).2) s x \bigr).$$$
Lean4
theorem mdifferentiableWithinAt_snd_comp_iff₂ {e e' : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e]
[MemTrivializationAtlas e'] {f : M → TotalSpace F E} {s : Set M} {x₀ : M} (hex₀ : f x₀ ∈ e.source)
(he'x₀ : f x₀ ∈ e'.source) (hf : MDifferentiableWithinAt IM IB (π F E ∘ f) s x₀) :
MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) s x₀ ↔
MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun x ↦ (e' (f x)).2) s x₀ :=
⟨(hf.change_section_trivialization IB · hex₀ he'x₀), (hf.change_section_trivialization IB · he'x₀ hex₀)⟩
