Theorems · Inductive type · algebraic topology

Bundle.ContinuousRiemannianMetric

{B : Type u_4} →
  [inst : TopologicalSpace B] →
    (F : Type u_5) →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] →
          (E : B → Type u_6) →
            [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
              [inst_4 : (b : B) → TopologicalSpace (E b)] →
                [inst_5 : (b : B) → AddCommGroup (E b)] →
                  [inst_6 : (b : B) → Module ℝ (E b)] →
                    [inst_7 : FiberBundle F E] → [VectorBundle ℝ F E] → Type (max u_4 u_6)

A family of inner product space structures on the fibers of a fiber bundle, defining the same topology as the already existing one, and varying continuously with the base point. See also ContMDiffRiemannianMetric for a smooth version. This structure is used through RiemannianBundle for typeclass inference, to register the inner product space structure on the fibers without creating diamonds.

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceAddCommGroupModuleFiberBundleVectorBundle