Theorems · Definition · algebraic topology

Bundle.ContinuousRiemannianMetric.ctorIdx

{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 → ℕ

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

0 results in Mathlib

Foundations

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