inner_bundle — Mathlib

English

The pointwise inner product of two differentiable maps into a Riemannian bundle is differentiable at a point.

Русский

Точечное скалярное произведение двух дифференцируемых векторов в риманиановом расслоении дифференцируемо в заданной точке.

LaTeX

$$Theorem: If hv and hw are differentiable at x in coordinates, then the inner product map x ↦ ⟪v(x), w(x)⟫ is differentiable at x.$$

Lean4

/-- Given two smooth maps into the same fibers of a Riemannian bundle,
their scalar product is smooth. -/
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 :=
  ContMDiffWithinAt.inner_bundle hv hw

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