Theorems · Theorem · algebraic topology

ContinuousWithinAt.inner_bundle

∀ {B : Type u_1} [inst : TopologicalSpace B] {F : Type u_2} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_3} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E] {M : Type u_4}
  [inst_8 : TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M}
  {x : M},
  ContinuousWithinAt (fun m => ⟨b m, v m⟩) s x →
    ContinuousWithinAt (fun m => ⟨b m, w m⟩) s x → ContinuousWithinAt (fun m => inner ℝ (v m) (w m)) s x

Given two continuous maps into the same fibers of a continuous Riemannian bundle, their inner product is continuous. Version with ContinuousWithinAt.

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleTopologicalSpaceIsContinuousRiemannianBundle