Theorems · Theorem · global analysis

MDifferentiableWithinAt.inner_bundle

∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  {EM : Type u_6} [inst_12 : NormedAddCommGroup EM] [inst_13 : NormedSpace ℝ EM] {HM : Type u_7}
  [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [inst_15 : TopologicalSpace M]
  [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)}
  {s : Set M} {x : M},
  (MDiffAt[s] fun m => ⟨b m, v m⟩) x → (MDiffAt[s] fun m => ⟨b m, w m⟩) x → (MDiffAt[s] fun m => inner ℝ (v m) (w m)) x

Given two differentiable maps into the same fibers of a Riemannian bundle, their scalar product is differentiable.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Cited by

2 results in Mathlib

Foundations

Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsContMDiffRiemannianBundle