inner_bundle — Mathlib

English

Compositions of smooth structures with ENat-indexed models yield a chain of contMDiffRiemannianBundle instances.

Русский

Составные структуры гладкости с ENat индексацией дают цепочку инстансов contMDiffRiemannianBundle.

LaTeX

$$$\\text{instIsContMDiffRiemannianBundle} (IB) (n) (F) (E)$$$

Lean4

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

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