Theorems · Inductive type · algebraic topology

Bundle.RiemannianMetric

{B : Type u_4} →
  (E : B → Type u_6) →
    [(b : B) → TopologicalSpace (E b)] →
      [inst : (b : B) → AddCommGroup (E b)] → [(b : B) → Module ℝ (E b)] → 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. This family is not assumed to be continuous or smooth: to guarantee continuity, resp. smoothness, of the inner product as a function of the base point, use ContinuousRiemannianMetric or ContMDiffRiemannianMetric. 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 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddCommGroupModule