Theorems · Theorem · differential geometry

CovariantDerivative.isMetricCompatible_iff

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V]
  [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : IsManifold I 1 M] [inst_15 : FiniteDimensional ℝ F],
  cov.IsMetricCompatible ↔
    ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
      MDiffAt (T% X) x →
        MDiffAt (T% σ) x →
          MDiffAt (T% τ) x →
            ((d% fun x => inner ℝ (σ x) (τ x)) x) (X x) =
              (fun x => inner ℝ ((fun x => (↑cov σ x) (X x)) x) (τ x)) x +
                (fun x => inner ℝ (σ x) ((fun x => (↑cov τ x) (X x)) x)) x

Defined in

Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleIsContMDiffRiemannianBundleContMDiffVectorBundleIsManifoldFiniteDimensional