English
If a function is MDifferentiableWithinAt, its fiber-coordinate composed with a base map via a trivialization is differentiable within the same domain, under base-set memberships.
Русский
Если функция дифференцируема внутри области, тогда координаты волокна после композиции через тривиализацию дифференцируемы в той же области при логических условиях принадлежности к базовым множествам.
LaTeX
$$$\displaystyle MDifferentiableWithinAt IM IB f s x \land Set.MapsTo f s e.baseSet \land Set.MapsTo f s e'.baseSet \Rightarrow MDifferentiableWithinAt IM (modelWithCornersSelf 𝕜 (ContinuousLinearMap (RingHom.id 𝕜) F F)) (\lambda y. (Trivialization.coordChangeL 𝕜 e e' (f y)).toContinuousLinearMap) s x.$$$
Lean4
theorem mdifferentiableOn_add_section (hs : MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u)
(ht : MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t x)) u) :
MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x ((s + t) x)) u := fun x₀ hx₀ ↦
mdifferentiableWithinAt_add_section (hs x₀ hx₀) (ht x₀ hx₀)
