Theorems · Inductive type · algebraic topology

IsContinuousRiemannianBundle

{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] → [VectorBundle ℝ F E] → Prop

Consider a real vector bundle in which each fiber is endowed with an inner product. We say that the bundle is Riemannian if the inner product depends continuously on the base point. This assumption is spelled IsContinuousRiemannianBundle F E where F is the model fiber, and E : B → Type* is the bundle.

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

20 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundle