Theorems · Inductive type · algebraic topology

ContMDiffVectorBundle

WithTop ℕ∞ →
  {𝕜 : Type u_1} →
    {B : Type u_2} →
      (F : Type u_4) →
        (E : B → Type u_6) →
          [inst : NontriviallyNormedField 𝕜] →
            {EB : Type u_7} →
              [inst_1 : NormedAddCommGroup EB] →
                [inst_2 : NormedSpace 𝕜 EB] →
                  {HB : Type u_8} →
                    [inst_3 : TopologicalSpace HB] →
                      ModelWithCorners 𝕜 EB HB →
                        [inst_4 : TopologicalSpace B] →
                          [ChartedSpace HB B] →
                            [inst_6 : (x : B) → AddCommMonoid (E x)] →
                              [inst_7 : (x : B) → Module 𝕜 (E x)] →
                                [inst_8 : NormedAddCommGroup F] →
                                  [inst_9 : NormedSpace 𝕜 F] →
                                    [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)] →
                                      [inst_11 : (x : B) → TopologicalSpace (E x)] →
                                        [inst_12 : FiberBundle F E] → [VectorBundle 𝕜 F E] → Prop

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

Cited by

106 results in Mathlib

Foundations

Depth 46 from the axioms, rests on 433 definitions · uses propext, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceAddCommMonoidModuleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceFiberBundleVectorBundle