English
Characterization of differentiability of a map into the total space in terms of base-projection and fiber-coordinates, using a trivialization, at a point within the base region.
Русский
Характеризация дифференцируемости отображения в полное пространство через проекцию на основание и координаты волокна с использованием тривиализации в точке внутри области.
LaTeX
$$$\displaystyle MDifferentiableWithinAt\! IM IB f s x \iff MDifferentiableWithinAt IM IB (\lambda y. (f y).proj) s x \land MDifferentiableWithinAt IM 𝓘(𝕜, F) (\lambda y. (e (f y)).2) s x.$$$
Lean4
theorem mdifferentiableWithinAt_neg_section
(hs : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u x₀) :
MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (-s x)) u x₀ :=
by
rw [mdifferentiableWithinAt_section] at hs ⊢
set e := trivializationAt F E x₀
refine hs.neg.congr_of_eventuallyEq ?_ ?_
· apply eventually_of_mem (U := e.baseSet)
· exact mem_nhdsWithin_of_mem_nhds <| (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F E x₀)
· exact fun x hx ↦ (e.linear 𝕜 hx).map_neg ..
· exact (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).map_neg ..
