Theorems · Definition · algebraic topology

Bundle.RiemannianBundle.recOn

{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)] →
          {motive : Bundle.RiemannianBundle E → Sort u} →
            (t : Bundle.RiemannianBundle E) → ((g : Bundle.RiemannianMetric E) → motive { g := g }) → motive t

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommGroupModule