inner_bundle — Mathlib

English

A trivial bundle with a fiber carrying a scalar product is a Riemannian bundle.

Русский

Тривиальное расслоение с фибром, несущим скалярное произведение, является риммановой связкой.

LaTeX

$$$\\text{IsContMDiffRiemannianBundle IB n F_1 (Bundle.Trivial B F_1)}$$$

Lean4

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

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