Structures · Geometry

ContMDiffVectorBundle

When B is a manifold with respect to a model IB and E is a topological vector bundle over B with fibers isomorphic to F, then ContMDiffVectorBundle n F E IB registers that the bundle is C^n, in the sense of having C^n transition functions. This is a mixin, not carrying any new data.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Basic

Shape

4 explicit arguments · adds contMDiffOn_coordChangeL