English
For a fixed trivialization, differentiability of a section on its base set is equivalent to differentiability of the fiber-projected component in the trivialization on that base set.
Русский
Для фиксированной тривиализации дифференцируемость секции на её базовом множестве эквивалентна дифференцируемости волокнистой части в тривиализации на этом базовом множестве.
LaTeX
$$$\displaystyle MDifferentiableOn IM (IB.prod 𝓘(𝕜, F)) (\lambda x. TotalSpace.mk' F x (s x)) e.baseSet \iff MDifferentiableOn IM 𝓘(𝕜, F) (\lambda x. (e (⟨x, s x⟩)).2) e.baseSet.$$$
Lean4
/-- For any trivialization `e`, the differentiability of a section on `e.baseSet`
can be determined using `e`. -/
theorem mdifferentiableOn_section_baseSet_iff {s : ∀ x, E x}
(e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B)) [MemTrivializationAtlas e] :
MDifferentiableOn IB (IB.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) e.baseSet ↔
MDifferentiableOn IB 𝓘(𝕜, F) (fun x ↦ (e ⟨x, s x⟩).2) e.baseSet :=
e.mdifferentiableOn_section_iff e.open_baseSet subset_rfl
