Theorems · Definition · algebraic topology

Bundle.ContinuousRiemannianMetric.inner

{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] →
                      [inst_8 : VectorBundle ℝ F E] →
                        Bundle.ContinuousRiemannianMetric F E → (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ

The inner product along the fibers of the bundle.

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceAddCommGroupModuleFiberBundleVectorBundle