{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)] →
          (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) →
            (∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v) →
              (∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v) →
                (∀ (b : B), ContinuousAt (fun v => ((inner b) v) v) 0) →
                  (∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}) → Bundle.RiemannianMetric E