inner_bundle — Mathlib

English

The inner product of two MDifferentiableWithinAt maps into a Riemannian bundle is MDifferentiableWithinAt.

Русский

Скалярное произведение двух отображений, дифференцируемых в окрестности, дифференцируемо в окрестности.

LaTeX

$$Is continuous: MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ,F)) n (v, w) -> MDifferentiableWithinAt IM 𝓘(ℝ) n ⟪v, w⟫$$

Lean4

/-- Given two smooth maps into the same fibers of a Riemannian bundle,
their scalar product is smooth. -/
theorem inner_bundle (hv : ContMDiffOn IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E)) s)
    (hw : ContMDiffOn IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E)) s) :
    ContMDiffOn IM 𝓘(ℝ) n (fun b ↦ ⟪v b, w b⟫) s := fun x hx ↦ (hv x hx).inner_bundle (hw x hx)

Похожие утверждения