English
Under a differential setup, the scalar product of two bundles is differentiable at a point.
Русский
В точке скалярное произведение двух секций дифференцируемо.
LaTeX
$$theorem inner_bundle (hv : ContMDiffAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E)) x) (hw : ContMDiffAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E)) x) : ContMDiffAt IM 𝓘(ℝ) n (fun b ↦ ⟪v b, w b⟫) x$$
Lean4
theorem add_section (hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u x₀)
(ht : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t x)) u x₀) :
ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s + t) x)) u x₀ :=
by
rw [contMDiffWithinAt_section] at hs ht ⊢
set e := trivializationAt F V x₀
refine (hs.add ht).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 V x₀)
· intro x hx
apply (e.linear 𝕜 hx).1
· apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).1
