Theorems · Definition · algebraic topology

Bundle.RiemannianBundle.g

{B : Type u_4} →
  {E : B → Type u_6} →
    {inst : (b : B) → TopologicalSpace (E b)} →
      {inst_1 : (b : B) → AddCommGroup (E b)} →
        {inst_2 : (b : B) → Module ℝ (E b)} → [self : Bundle.RiemannianBundle E] → Bundle.RiemannianMetric E

The family of inner products on the fibers

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

0 results in Mathlib

Foundations

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

Assumes

Bundle.RiemannianBundle