Theorems · Inductive type · algebraic topology

VectorPrebundle.IsContMDiff

{𝕜 : 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 : (x : B) → TopologicalSpace (E x)] →
                                    VectorPrebundle 𝕜 F E → WithTop ℕ∞ → Prop

Mixin for a VectorPrebundle stating that coordinate changes are C^n.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Basic

Cited by

5 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceAddCommMonoidModuleNormedAddCommGroupNormedSpaceTopologicalSpace