Theorems · Theorem · algebraic topology

VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange

∀ {𝕜 : 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}
  {IB : ModelWithCorners 𝕜 EB HB} {inst_4 : TopologicalSpace B} {inst_5 : 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)} {a : VectorPrebundle 𝕜 F E} {n : WithTop ℕ∞}
  [self : VectorPrebundle.IsContMDiff IB a n],
  ∀ e ∈ a.pretrivializationAtlas,
    ∀ e' ∈ a.pretrivializationAtlas,
      ∃ f,
        ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n f (e.baseSet ∩ e'.baseSet) ∧
          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2

Defined in

Mathlib.Geometry.Manifold.VectorBundle.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

VectorPrebundle.IsContMDiff