English
If two maps are MDifferentiableOn a set, their fiberwise inner product is also differentiableOn that set.
Русский
Если две карты дифференцируемы на множестве, их волокно-привязанное скалярное произведение также дифференцируемо на этом множестве.
LaTeX
$$MDifferentiableOn IM (IB.prod 𝓘(ℝ,F)) n (v) s ∧ MDifferentiableOn IM (IB.prod 𝓘(ℝ,F)) n (w) s ⇒ MDifferentiableOn IM 𝓘(ℝ) n (λ x, ⟪v x, w x⟫) s$$
Lean4
/-- Given two differentiable maps into the same fibers of a Riemannian bundle,
their scalar product is differentiable. -/
theorem inner_bundle (hv : MDifferentiableOn IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (v m : TotalSpace F E)) s)
(hw : MDifferentiableOn IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (w m : TotalSpace F E)) s) :
MDifferentiableOn IM 𝓘(ℝ) (fun b ↦ ⟪v b, w b⟫) s := fun x hx ↦ (hv x hx).inner_bundle (hw x hx)
