C^n vector bundles

This file defines C^n vector bundles over a manifold.

Let E be a topological vector bundle, with model fiber F and base space B. We consider E as carrying a charted space structure given by its trivializations -- these are charts to B × F. Then, by "composition", if B is itself a charted space over H (e.g. a smooth manifold), then E is also a charted space over H × F.

Now, we define ContMDiffVectorBundle as the Prop of having C^n transition functions. Recall the structure groupoid contMDiffFiberwiseLinear on B × F consisting of C^n, fiberwise linear open partial homeomorphisms. We show that our definition of "C^n vector bundle" implies HasGroupoid for this groupoid, and show (by a "composition" of HasGroupoid instances) that this means that a C^n vector bundle is a C^n manifold.

Since ContMDiffVectorBundle is a mixin, it should be easy to make variants and for many such variants to coexist -- vector bundles can be C^n vector bundles over several different base fields, etc.

Main definitions and constructions

• FiberBundle.chartedSpace: A fiber bundle E over a base B with model fiber F is naturally a charted space modelled on B × F.

• FiberBundle.chartedSpace': Let B be a charted space modelled on HB. Then a fiber bundle E over a base B with model fiber F is naturally a charted space modelled on HB.prod F.

• ContMDiffVectorBundle: Mixin class stating that a (topological) VectorBundle is C^n, in the sense of having C^n transition functions, where the smoothness index n belongs to WithTop ℕ∞.

• ContMDiffFiberwiseLinear.hasGroupoid: For a C^n vector bundle E over B with fiber modelled on F, the change-of-co-ordinates between two trivializations e, e' for E, considered as charts to B × F, is C^n and fiberwise linear, in the sense of belonging to the structure groupoid contMDiffFiberwiseLinear.

• Bundle.TotalSpace.isManifold: A C^n vector bundle is naturally a C^n manifold.

• VectorBundleCore.instContMDiffVectorBundle: If a (topological) VectorBundleCore is C^n, in the sense of having C^n transition functions (cf. VectorBundleCore.IsContMDiff), then the vector bundle constructed from it is a C^n vector bundle.

• VectorPrebundle.contMDiffVectorBundle: If a VectorPrebundle is C^n, in the sense of having C^n transition functions (cf. VectorPrebundle.IsContMDiff), then the vector bundle constructed from it is a C^n vector bundle.

• Bundle.Prod.contMDiffVectorBundle: The direct sum of two C^n vector bundles is a C^n vector bundle.

Charted space structure on a fiber bundle

instance FiberBundle.chartedSpace' {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [TopologicalSpace B] [FiberBundle F E] : ChartedSpace (B × F) (Bundle.TotalSpace F E)

A fiber bundle E over a base B with model fiber F is naturally a charted space modelled on B × F.

Equations

• One or more equations did not get rendered due to their size.

theorem FiberBundle.chartedSpace'_chartAt {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [TopologicalSpace B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : chartAt (B × F) x = (trivializationAt F E x.proj).toOpenPartialHomeomorph

instance FiberBundle.chartedSpace {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] : ChartedSpace (ModelProd HB F) (Bundle.TotalSpace F E)

Let B be a charted space modelled on HB. Then a fiber bundle E over a base B with model fiber F is naturally a charted space modelled on HB.prod F.

Equations

• FiberBundle.chartedSpace = ChartedSpace.comp (ModelProd HB F) (B × F) (Bundle.TotalSpace F E)

theorem FiberBundle.chartedSpace_chartAt {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : chartAt (ModelProd HB F) x = (trivializationAt F E x.proj).trans ((chartAt HB x.proj).prod (OpenPartialHomeomorph.refl F))

theorem FiberBundle.chartedSpace_chartAt_symm_fst {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {HB : Type u_7} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) (y : ModelProd HB F) (hy : y ∈ (chartAt (ModelProd HB F) x).target) : (↑(chartAt (ModelProd HB F) x).symm y).proj = ↑(chartAt HB x.proj).symm y.1

theorem FiberBundle.extChartAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x = (trivializationAt F E x.proj).trans ((extChartAt IB x.proj).prod (PartialEquiv.refl F))

theorem FiberBundle.extChartAt_target {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] (x : Bundle.TotalSpace F E) : (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x).target = ((extChartAt IB x.proj).target ∩ ↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ Set.univ

theorem FiberBundle.writtenInExtChartAt_trivializationAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {x : Bundle.TotalSpace F E} {y : EB × F} (hy : y ∈ (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x).target) : writtenInExtChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) x (↑(trivializationAt F E x.proj)) y = y

theorem FiberBundle.writtenInExtChartAt_trivializationAt_symm {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {x : Bundle.TotalSpace F E} {y : EB × F} (hy : y ∈ (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x).target) : writtenInExtChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) (↑(trivializationAt F E x.proj) x) (↑(trivializationAt F E x.proj).symm) y = y

Regularity of maps in/out fiber bundles

Note: For these results we don't need that the bundle is a C^n vector bundle, or even a vector bundle at all, just that it is a fiber bundle over a charted base space.

theorem Bundle.contMDiffWithinAt_totalSpace {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_11} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {f : M → TotalSpace F E} {s : Set M} {x₀ : M} : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀

Characterization of C^n functions into a vector bundle. Version at a point within a set.

theorem Bundle.contMDiffAt_totalSpace {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {EM : Type u_10} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_11} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {f : M → TotalSpace F E} {x₀ : M} : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f x₀ ↔ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ∧ ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Characterization of C^n functions into a vector bundle. Version at a point.

theorem Bundle.contMDiffWithinAt_section {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : (x : B) → E x} {a : Set B} {x₀ : B} : ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => TotalSpace.mk' F x (s x)) a x₀ ↔ ContMDiffWithinAt IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) a x₀

Characterization of C^n sections within a set at a point of a vector bundle.

theorem Bundle.contMDiffAt_section {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : (x : B) → E x} (x₀ : B) : ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => TotalSpace.mk' F x (s x)) x₀ ↔ ContMDiffAt IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) x₀

Characterization of C^n sections of a vector bundle.

theorem Bundle.contMDiff_proj {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] : ContMDiff (IB.prod (modelWithCornersSelf 𝕜 F)) IB n TotalSpace.proj

theorem Bundle.contMDiffOn_proj {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (TotalSpace F E)} : ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) IB n TotalSpace.proj s

theorem Bundle.contMDiffAt_proj {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {p : TotalSpace F E} : ContMDiffAt (IB.prod (modelWithCornersSelf 𝕜 F)) IB n TotalSpace.proj p

theorem Bundle.contMDiffWithinAt_proj {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] {s : Set (TotalSpace F E)} {p : TotalSpace F E} : ContMDiffWithinAt (IB.prod (modelWithCornersSelf 𝕜 F)) IB n TotalSpace.proj s p

theorem Bundle.contMDiff_zeroSection {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] : ContMDiff IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (zeroSection F E)

theorem Bundle.contMDiffOn_zeroSection {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B} : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (zeroSection F E) t

theorem Bundle.contMDiffAt_zeroSection {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {x : B} : ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (zeroSection F E) x

theorem Bundle.contMDiffWithinAt_zeroSection {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F E] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B} {x : B} : ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (zeroSection F E) t x

C^n vector bundles

class ContMDiffVectorBundle (n : WithTop ℕ∞) {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [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.

• contMDiffOn_coordChangeL (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

theorem ContMDiffVectorBundle.of_le {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] {m n : WithTop ℕ∞} (hmn : m ≤ n) [h : ContMDiffVectorBundle n F E IB] : ContMDiffVectorBundle m F E IB

instance instContMDiffVectorBundleOfSomeENatTopOfLEInfty {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] {a : WithTop ℕ∞} [ContMDiffVectorBundle (↑⊤) F E IB] [h : ENat.LEInfty a] : ContMDiffVectorBundle a F E IB

instance instContMDiffVectorBundleOfTopWithTopENat {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] {a : WithTop ℕ∞} [ContMDiffVectorBundle ⊤ F E IB] : ContMDiffVectorBundle a F E IB

instance instContMDiffVectorBundleOfNatWithTopENat {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle 2 F E IB] : ContMDiffVectorBundle 1 F E IB

instance instContMDiffVectorBundleOfNatWithTopENat_1 {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] : ContMDiffVectorBundle 0 F E IB

theorem contMDiffOn_coordChangeL {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

theorem contMDiffOn_symm_coordChangeL {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm) (e.baseSet ∩ e'.baseSet)

theorem contMDiffAt_coordChangeL {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) : ContMDiffAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (b : B) => ↑(Trivialization.coordChangeL 𝕜 e e' b)) x

theorem ContMDiffWithinAt.coordChangeL {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {x : M} (hf : ContMDiffWithinAt IM IB n f s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) s x

theorem ContMDiffAt.coordChangeL {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {x : M} (hf : ContMDiffAt IM IB n f x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : ContMDiffAt IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) x

theorem ContMDiffOn.coordChangeL {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} (hf : ContMDiffOn IM IB n f s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) : ContMDiffOn IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) s

theorem ContMDiff.coordChangeL {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} (hf : ContMDiff IM IB n f) (he : ∀ (x : M), f x ∈ e.baseSet) (he' : ∀ (x : M), f x ∈ e'.baseSet) : ContMDiff IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n fun (y : M) => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))

theorem ContMDiffWithinAt.coordChange {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F} {x : M} (hf : ContMDiffWithinAt IM IB n f s x) (hg : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n g s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => e.coordChange e' (f y) (g y)) s x

theorem ContMDiffAt.coordChange {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {g : M → F} {x : M} (hf : ContMDiffAt IM IB n f x) (hg : ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n g x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) : ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => e.coordChange e' (f y) (g y)) x

theorem ContMDiffOn.coordChange {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F} (hf : ContMDiffOn IM IB n f s) (hg : ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n g s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) : ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => e.coordChange e' (f y) (g y)) s

theorem ContMDiff.coordChange {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M → B} {g : M → F} (hf : ContMDiff IM IB n f) (hg : ContMDiff IM (modelWithCornersSelf 𝕜 F) n g) (he : ∀ (x : M), f x ∈ e.baseSet) (he' : ∀ (x : M), f x ∈ e'.baseSet) : ContMDiff IM (modelWithCornersSelf 𝕜 F) n fun (y : M) => e.coordChange e' (f y) (g y)

theorem Trivialization.contMDiffOn_symm_trans {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (↑(e.symm.trans e'.toOpenPartialHomeomorph)) (e.target ∩ e'.target)

theorem ContMDiffWithinAt.change_section_trivialization {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {x : M} {f : M → Bundle.TotalSpace F E} (hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x) (hf : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e (f y)).2) s x) (he : f x ∈ e.source) (he' : f x ∈ e'.source) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e' (f y)).2) s x

theorem Trivialization.contMDiffWithinAt_snd_comp_iff₂ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {s : Set M} {x : M} {f : M → Bundle.TotalSpace F E} (hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x) (he : f x ∈ e.source) (he' : f x ∈ e'.source) : ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e (f y)).2) s x ↔ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (y : M) => (↑e' (f y)).2) s x

instance ContMDiffFiberwiseLinear.hasGroupoid {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] : HasGroupoid (Bundle.TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)

For a C^n vector bundle E over B with fiber modelled on F, the change-of-co-ordinates between two trivializations e, e' for E, considered as charts to B × F, is C^n and fiberwise linear.

instance Bundle.TotalSpace.isManifold {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] [IsManifold IB n B] : IsManifold (IB.prod (modelWithCornersSelf 𝕜 F)) n (TotalSpace F E)

A C^n vector bundle E is naturally a C^n manifold.

theorem Trivialization.contMDiffWithinAt_iff {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {s : Set M} {x₀ : M} (he : f x₀ ∈ e.source) : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun (x : M) => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (↑e (f x)).2) s x₀

theorem Trivialization.contMDiffAt_iff {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) : ContMDiffAt IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f x₀ ↔ ContMDiffAt IM IB n (fun (x : M) => (f x).proj) x₀ ∧ ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (↑e (f x)).2) x₀

theorem Trivialization.contMDiffOn_iff {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} {s : Set M} (he : Set.MapsTo f s e.source) : ContMDiffOn IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f s ↔ ContMDiffOn IM IB n (fun (x : M) => (f x).proj) s ∧ ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (↑e (f x)).2) s

theorem Trivialization.contMDiff_iff {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type u_9} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_10} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {f : M → Bundle.TotalSpace F E} (he : ∀ (x : M), f x ∈ e.source) : ContMDiff IM (IB.prod (modelWithCornersSelf 𝕜 F)) n f ↔ (ContMDiff IM IB n fun (x : M) => (f x).proj) ∧ ContMDiff IM (modelWithCornersSelf 𝕜 F) n fun (x : M) => (↑e (f x)).2

theorem Trivialization.contMDiffOn {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (↑e) e.source

theorem Trivialization.contMDiffOn_symm {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (↑e.symm) e.target

theorem Trivialization.contMDiffWithinAt_section {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} (a : Set B) {x₀ : B} {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] (hx₀ : x₀ ∈ e.baseSet) : ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) a x₀ ↔ ContMDiffWithinAt IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e { proj := x, snd := s x }).2) a x₀

Smoothness of a C^n section at x₀ within a set a can be determined using any trivialisation whose baseSet contains x₀.

theorem Trivialization.contMDiffAt_section_iff {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} {x₀ : B} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (hx₀ : x₀ ∈ e.baseSet) : ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) x₀ ↔ ContMDiffAt IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e { proj := x, snd := s x }).2) x₀

Smoothness of a C^n section at x₀ can be determined using any trivialisation whose baseSet contains x₀.

@[deprecated Trivialization.contMDiffAt_section_iff (since := "2025-09-15")]

theorem contMDiffAt_section_of_mem_baseSet {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} {x₀ : B} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (hx₀ : x₀ ∈ e.baseSet) : ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) x₀ ↔ ContMDiffAt IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e { proj := x, snd := s x }).2) x₀

Alias of Trivialization.contMDiffAt_section_iff.

---

Smoothness of a C^n section at x₀ can be determined using any trivialisation whose baseSet contains x₀.

theorem Trivialization.contMDiffOn_section_iff {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} {a : Set B} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (ha : IsOpen a) (ha' : a ⊆ e.baseSet) : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) a ↔ ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e { proj := x, snd := s x }).2) a

Smoothness of a C^n section on s can be determined using any trivialisation whose baseSet contains s.

@[deprecated Trivialization.contMDiffOn_section_iff (since := "2025-09-15")]

theorem contMDiffOn_section_of_mem_baseSet {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} {a : Set B} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (ha : IsOpen a) (ha' : a ⊆ e.baseSet) : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) a ↔ ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e { proj := x, snd := s x }).2) a

Alias of Trivialization.contMDiffOn_section_iff.

---

Smoothness of a C^n section on s can be determined using any trivialisation whose baseSet contains s.

theorem Trivialization.contMDiffOn_section_baseSet_iff {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) e.baseSet ↔ ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e { proj := x, snd := s x }).2) e.baseSet

For any trivialization e, the smoothness of a C^n section on e.baseSet can be determined using e.

@[deprecated Trivialization.contMDiffOn_section_baseSet_iff (since := "2025-09-15")]

theorem contMDiffOn_section_of_mem_baseSet₀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E] [ContMDiffVectorBundle n F E IB] {s : (x : B) → E x} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] : ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) e.baseSet ↔ ContMDiffOn IB (modelWithCornersSelf 𝕜 F) n (fun (x : B) => (↑e { proj := x, snd := s x }).2) e.baseSet

Alias of Trivialization.contMDiffOn_section_baseSet_iff.

---

For any trivialization e, the smoothness of a C^n section on e.baseSet can be determined using e.

Core construction for C^n vector bundles

class VectorBundleCore.IsContMDiff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) (IB : ModelWithCorners 𝕜 EB HB) (n : WithTop ℕ∞) : Prop

Mixin for a VectorBundleCore stating that transition functions are C^n.

• contMDiffOn_coordChange (i j : ι) : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)

theorem VectorBundleCore.contMDiffOn_coordChange {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) (IB : ModelWithCorners 𝕜 EB HB) [h : Z.IsContMDiff IB n] (i j : ι) : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j)

instance VectorBundleCore.instContMDiffVectorBundle {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι) [Z.IsContMDiff IB n] : ContMDiffVectorBundle n F Z.Fiber IB

If a VectorBundleCore has the IsContMDiff mixin, then the vector bundle constructed from it is a C^n vector bundle.

The trivial C^n vector bundle

instance Bundle.Trivial.contMDiffVectorBundle {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : ContMDiffVectorBundle n F (Trivial B F) IB

A trivial vector bundle over a manifold is a C^n vector bundle.

Direct sums of C^n vector bundles

instance Bundle.Prod.contMDiffVectorBundle {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] (F₁ : Type u_11) [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] (E₁ : B → Type u_12) [TopologicalSpace (TotalSpace F₁ E₁)] [(x : B) → AddCommMonoid (E₁ x)] [(x : B) → Module 𝕜 (E₁ x)] (F₂ : Type u_13) [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] (E₂ : B → Type u_14) [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B) → AddCommMonoid (E₂ x)] [(x : B) → Module 𝕜 (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ E₂] [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB] : ContMDiffVectorBundle n (F₁ × F₂) (fun (x : B) => E₁ x × E₂ x) IB

The direct sum of two C^n vector bundles over the same base is a C^n vector bundle.

Prebundle construction for C^n vector bundles

class VectorPrebundle.IsContMDiff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) (n : WithTop ℕ∞) : Prop

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

• exists_contMDiffCoordChange (e : Pretrivialization F Bundle.TotalSpace.proj) : e ∈ a.pretrivializationAtlas → ∀ e' ∈ a.pretrivializationAtlas, ∃ (f : B → F →L[𝕜] F), ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n f (e.baseSet ∩ e'.baseSet) ∧ ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' { proj := b, snd := e.symm b v }).2

noncomputable def VectorPrebundle.contMDiffCoordChange (n : WithTop ℕ∞) {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : IsContMDiff IB a n] {e e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) (b : B) : F →L[𝕜] F

A randomly chosen coordinate change on a VectorPrebundle satisfying IsContMDiff, given by the field exists_coordChange. Note that a.contMDiffCoordChange need not be the same as a.coordChange.

Equations

• VectorPrebundle.contMDiffCoordChange n IB a he he' b = Classical.choose ⋯ b

theorem VectorPrebundle.contMDiffOn_contMDiffCoordChange {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : IsContMDiff IB a n] {e e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (contMDiffCoordChange n IB a he he') (e.baseSet ∩ e'.baseSet)

theorem VectorPrebundle.contMDiffCoordChange_apply {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : IsContMDiff IB a n] {e e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet) (v : F) : (contMDiffCoordChange n IB a he he' b) v = (↑e' { proj := b, snd := e.symm b v }).2

theorem VectorPrebundle.mk_contMDiffCoordChange {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : IsContMDiff IB a n] {e e' : Pretrivialization F Bundle.TotalSpace.proj} (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet) (v : F) : (b, (contMDiffCoordChange n IB a he he' b) v) = ↑e' { proj := b, snd := e.symm b v }

theorem VectorPrebundle.contMDiffVectorBundle {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [NontriviallyNormedField 𝕜] {EB : Type u_7} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_8} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] [(x : B) → AddCommMonoid (E x)] [(x : B) → Module 𝕜 (E x)] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [(x : B) → TopologicalSpace (E x)] (a : VectorPrebundle 𝕜 F E) [ha : IsContMDiff IB a n] : ContMDiffVectorBundle n F E IB

Make a ContMDiffVectorBundle from a ContMDiffVectorPrebundle.