Structures · Geometry

CovariantDerivative.ContMDiffCovariantDerivative

A covariant derivative ∇ is called of class C^k iff, whenever X is a C^k section and σ a C^{k+1} section, the result ∇_X σ is a C^k section. This is a class so typeclass inference can deduce this automatically. We will prove in a later file that any C^(k+1) covariant derivative is C^k.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Shape

2 explicit arguments · adds contMDiff