Theorems · Theorem · global analysis

IsContMDiffRiemannianBundle.exists_contMDiff

∀ {EB : Type u_1} {inst : NormedAddCommGroup EB} {inst_1 : NormedSpace ℝ EB} {HB : Type u_2}
  {inst_2 : TopologicalSpace HB} {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  {inst_3 : TopologicalSpace B} {inst_4 : ChartedSpace HB B} {F : Type u_4} {inst_5 : NormedAddCommGroup F}
  {inst_6 : NormedSpace ℝ F} {E : B → Type u_5} {inst_7 : TopologicalSpace (Bundle.TotalSpace F E)}
  {inst_8 : (x : B) → NormedAddCommGroup (E x)} {inst_9 : (x : B) → InnerProductSpace ℝ (E x)}
  {inst_10 : FiberBundle F E} {inst_11 : VectorBundle ℝ F E} [self : IsContMDiffRiemannianBundle IB n F E],
  ∃ g,
    (ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, g b⟩) ∧
      ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Cited by

3 results in Mathlib

Foundations

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

Assumes

IsContMDiffRiemannianBundle