Documentation

Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Differentiability of functions in vector bundles #

theorem mdifferentiableWithinAt_totalSpace {๐•œ : 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 (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) {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 โ†’ Bundle.TotalSpace F E) {s : Set M} {xโ‚€ : M} :
MDifferentiableWithinAt IM (IB.prod (modelWithCornersSelf ๐•œ F)) f s xโ‚€ โ†” MDifferentiableWithinAt IM IB (fun (x : M) => (f x).proj) s xโ‚€ โˆง MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘(trivializationAt F E (f xโ‚€).proj) (f x)).2) s xโ‚€

Characterization of differentiable functions into a vector bundle. Version at a point within a set

theorem mdifferentiableAt_totalSpace {๐•œ : 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 (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) {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 โ†’ Bundle.TotalSpace F E) {xโ‚€ : M} :
MDifferentiableAt IM (IB.prod (modelWithCornersSelf ๐•œ F)) f xโ‚€ โ†” MDifferentiableAt IM IB (fun (x : M) => (f x).proj) xโ‚€ โˆง MDifferentiableAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘(trivializationAt F E (f xโ‚€).proj) (f x)).2) xโ‚€

Characterization of differentiable functions into a vector bundle. Version at a point

theorem mdifferentiableWithinAt_section {๐•œ : 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] (s : (b : B) โ†’ E b) {u : Set B} {bโ‚€ : B} :
MDifferentiableWithinAt IB (IB.prod (modelWithCornersSelf ๐•œ F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) u bโ‚€ โ†” MDifferentiableWithinAt IB (modelWithCornersSelf ๐•œ F) (fun (b : B) => (โ†‘(trivializationAt F E bโ‚€) { proj := b, snd := s b }).2) u bโ‚€

Characterization of differentiable sections of a vector bundle at a point within a set in terms of the preferred trivialization at that point.

theorem mdifferentiableAt_section {๐•œ : 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] (s : (b : B) โ†’ E b) {bโ‚€ : B} :
MDifferentiableAt IB (IB.prod (modelWithCornersSelf ๐•œ F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) bโ‚€ โ†” MDifferentiableAt IB (modelWithCornersSelf ๐•œ F) (fun (b : B) => (โ†‘(trivializationAt F E bโ‚€) { proj := b, snd := s b }).2) bโ‚€

Characterization of differentiable sections of a vector bundle at a point within a set in terms of the preferred trivialization at that point.

theorem Bundle.mdifferentiable_proj {๐•œ : 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] :
theorem Bundle.mdifferentiableOn_proj {๐•œ : 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)} :
theorem Bundle.mdifferentiableAt_proj {๐•œ : 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} :
theorem Bundle.mdifferentiableWithinAt_proj {๐•œ : 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} :
theorem Bundle.mdifferentiable_zeroSection (๐•œ : 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] :
theorem Bundle.mdifferentiableOn_zeroSection (๐•œ : 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} :
theorem Bundle.mdifferentiableAt_zeroSection (๐•œ : 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} :
theorem Bundle.mdifferentiableWithinAt_zeroSection (๐•œ : 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} :
theorem mdifferentiableOn_coordChangeL {๐•œ : 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 : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] :
MDifferentiableOn IB (modelWithCornersSelf ๐•œ (F โ†’L[๐•œ] F)) (fun (b : B) => โ†‘(Trivialization.coordChangeL ๐•œ e e' b)) (e.baseSet โˆฉ e'.baseSet)
theorem mdifferentiableOn_symm_coordChangeL {๐•œ : 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 : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] (e e' : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] :
MDifferentiableOn IB (modelWithCornersSelf ๐•œ (F โ†’L[๐•œ] F)) (fun (b : B) => โ†‘(Trivialization.coordChangeL ๐•œ e e' b).symm) (e.baseSet โˆฉ e'.baseSet)
theorem mdifferentiableAt_coordChangeL {๐•œ : 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 : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {x : B} (h : x โˆˆ e.baseSet) (h' : x โˆˆ e'.baseSet) :
MDifferentiableAt IB (modelWithCornersSelf ๐•œ (F โ†’L[๐•œ] F)) (fun (b : B) => โ†‘(Trivialization.coordChangeL ๐•œ e e' b)) x
theorem MDifferentiableWithinAt.coordChangeL {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M โ†’ B} {x : M} (hf : MDifferentiableWithinAt IM IB f s x) (he : f x โˆˆ e.baseSet) (he' : f x โˆˆ e'.baseSet) :
MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ (F โ†’L[๐•œ] F)) (fun (y : M) => โ†‘(Trivialization.coordChangeL ๐•œ e e' (f y))) s x
theorem MDifferentiableAt.coordChangeL {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {f : M โ†’ B} {x : M} (hf : MDifferentiableAt IM IB f x) (he : f x โˆˆ e.baseSet) (he' : f x โˆˆ e'.baseSet) :
MDifferentiableAt IM (modelWithCornersSelf ๐•œ (F โ†’L[๐•œ] F)) (fun (y : M) => โ†‘(Trivialization.coordChangeL ๐•œ e e' (f y))) x
theorem MDifferentiableOn.coordChangeL {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M โ†’ B} (hf : MDifferentiableOn IM IB f s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) :
MDifferentiableOn IM (modelWithCornersSelf ๐•œ (F โ†’L[๐•œ] F)) (fun (y : M) => โ†‘(Trivialization.coordChangeL ๐•œ e e' (f y))) s
theorem MDifferentiable.coordChangeL {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {f : M โ†’ B} (hf : MDifferentiable IM IB f) (he : โˆ€ (x : M), f x โˆˆ e.baseSet) (he' : โˆ€ (x : M), f x โˆˆ e'.baseSet) :
MDifferentiable IM (modelWithCornersSelf ๐•œ (F โ†’L[๐•œ] F)) fun (y : M) => โ†‘(Trivialization.coordChangeL ๐•œ e e' (f y))
theorem MDifferentiableWithinAt.coordChange {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M โ†’ B} {g : M โ†’ F} {x : M} (hf : MDifferentiableWithinAt IM IB f s x) (hg : MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) g s x) (he : f x โˆˆ e.baseSet) (he' : f x โˆˆ e'.baseSet) :
MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) (fun (y : M) => e.coordChange e' (f y) (g y)) s x
theorem MDifferentiableAt.coordChange {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {f : M โ†’ B} {g : M โ†’ F} {x : M} (hf : MDifferentiableAt IM IB f x) (hg : MDifferentiableAt IM (modelWithCornersSelf ๐•œ F) g x) (he : f x โˆˆ e.baseSet) (he' : f x โˆˆ e'.baseSet) :
MDifferentiableAt IM (modelWithCornersSelf ๐•œ F) (fun (y : M) => e.coordChange e' (f y) (g y)) x
theorem MDifferentiableOn.coordChange {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {s : Set M} {f : M โ†’ B} {g : M โ†’ F} (hf : MDifferentiableOn IM IB f s) (hg : MDifferentiableOn IM (modelWithCornersSelf ๐•œ F) g s) (he : Set.MapsTo f s e.baseSet) (he' : Set.MapsTo f s e'.baseSet) :
MDifferentiableOn IM (modelWithCornersSelf ๐•œ F) (fun (y : M) => e.coordChange e' (f y) (g y)) s
theorem MDifferentiable.coordChange {๐•œ : 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 (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} {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {f : M โ†’ B} {g : M โ†’ F} (hf : MDifferentiable IM IB f) (hg : MDifferentiable IM (modelWithCornersSelf ๐•œ F) g) (he : โˆ€ (x : M), f x โˆˆ e.baseSet) (he' : โˆ€ (x : M), f x โˆˆ e'.baseSet) :
MDifferentiable IM (modelWithCornersSelf ๐•œ F) fun (y : M) => e.coordChange e' (f y) (g y)
theorem MDifferentiableWithinAt.change_section_trivialization {๐•œ : 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 (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) {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {e : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] {e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e'] {f : M โ†’ Bundle.TotalSpace F E} {s : Set M} {xโ‚€ : M} (hf : MDifferentiableWithinAt IM IB (Bundle.TotalSpace.proj โˆ˜ f) s xโ‚€) (he'f : MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e (f x)).2) s xโ‚€) (he : f xโ‚€ โˆˆ e.source) (he' : f xโ‚€ โˆˆ e'.source) :
MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e' (f x)).2) s xโ‚€
theorem Trivialization.mdifferentiableWithinAt_snd_comp_iffโ‚‚ {๐•œ : 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 (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) {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M โ†’ Bundle.TotalSpace F E} {s : Set M} {xโ‚€ : M} (hexโ‚€ : f xโ‚€ โˆˆ e.source) (he'xโ‚€ : f xโ‚€ โˆˆ e'.source) (hf : MDifferentiableWithinAt IM IB (Bundle.TotalSpace.proj โˆ˜ f) s xโ‚€) :
MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e (f x)).2) s xโ‚€ โ†” MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e' (f x)).2) s xโ‚€
theorem Trivialization.mdifferentiableAt_snd_comp_iffโ‚‚ {๐•œ : 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 (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) {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {e e' : Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e] [MemTrivializationAtlas e'] {f : M โ†’ Bundle.TotalSpace F E} {xโ‚€ : M} (he : f xโ‚€ โˆˆ e.source) (he' : f xโ‚€ โˆˆ e'.source) (hf : MDifferentiableAt IM IB (fun (x : M) => (f x).proj) xโ‚€) :
MDifferentiableAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e (f x)).2) xโ‚€ โ†” MDifferentiableAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e' (f x)).2) xโ‚€
theorem Trivialization.mdifferentiableWithinAt_totalSpace_iff {๐•œ : 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 (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) {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 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) :
MDifferentiableWithinAt IM (IB.prod (modelWithCornersSelf ๐•œ F)) f s xโ‚€ โ†” MDifferentiableWithinAt IM IB (fun (x : M) => (f x).proj) s xโ‚€ โˆง MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e (f x)).2) s xโ‚€

Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point within at set.

theorem Trivialization.mdifferentiableAt_totalSpace_iff {๐•œ : 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 (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) {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] [(x : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (f : M โ†’ Bundle.TotalSpace F E) {xโ‚€ : M} (he : f xโ‚€ โˆˆ e.source) :
MDifferentiableAt IM (IB.prod (modelWithCornersSelf ๐•œ F)) f xโ‚€ โ†” MDifferentiableAt IM IB (fun (x : M) => (f x).proj) xโ‚€ โˆง MDifferentiableAt IM (modelWithCornersSelf ๐•œ F) (fun (x : M) => (โ†‘e (f x)).2) xโ‚€

Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point.

theorem Trivialization.mdifferentiableWithinAt_section_iff {๐•œ : 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 : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (s : (b : B) โ†’ E b) {u : Set B} {bโ‚€ : B} (hexโ‚€ : bโ‚€ โˆˆ e.baseSet) :
MDifferentiableWithinAt IB (IB.prod (modelWithCornersSelf ๐•œ F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) u bโ‚€ โ†” MDifferentiableWithinAt IB (modelWithCornersSelf ๐•œ F) (fun (x : B) => (โ†‘e { proj := x, snd := s x }).2) u bโ‚€

Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point within at set.

theorem Trivialization.mdifferentiableAt_section_iff {๐•œ : 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 : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] (s : (b : B) โ†’ E b) {bโ‚€ : B} (hexโ‚€ : bโ‚€ โˆˆ e.baseSet) :
MDifferentiableAt IB (IB.prod (modelWithCornersSelf ๐•œ F)) (fun (b : B) => Bundle.TotalSpace.mk' F b (s b)) bโ‚€ โ†” MDifferentiableAt IB (modelWithCornersSelf ๐•œ F) (fun (x : B) => (โ†‘e { proj := x, snd := s x }).2) bโ‚€

Characterization of differentiable functions into a vector bundle in terms of any trivialization. Version at a point.

theorem Trivialization.mdifferentiableOn_section_iff {๐•œ : 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 : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 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) :
MDifferentiableOn IB (IB.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) a โ†” MDifferentiableOn IB (modelWithCornersSelf ๐•œ F) (fun (x : B) => (โ†‘e { proj := x, snd := s x }).2) a

Differentiability of a section on s can be determined using any trivialisation whose baseSet contains s.

theorem Trivialization.mdifferentiableOn_section_baseSet_iff {๐•œ : 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 : B) โ†’ AddCommMonoid (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] [ContMDiffVectorBundle 1 F E IB] {s : (x : B) โ†’ E x} (e : Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e] :
MDifferentiableOn IB (IB.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) e.baseSet โ†” MDifferentiableOn IB (modelWithCornersSelf ๐•œ F) (fun (x : B) => (โ†‘e { proj := x, snd := s x }).2) e.baseSet

For any trivialization e, the differentiability of a section on e.baseSet can be determined using e.

theorem mdifferentiableWithinAt_add_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} {u : Set B} {xโ‚€ : B} (hs : MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u xโ‚€) (ht : MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x ((s + t) x)) u xโ‚€
theorem mdifferentiableAt_add_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} {xโ‚€ : B} (hs : MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) xโ‚€) (ht : MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x ((s + t) x)) xโ‚€
theorem mdifferentiableOn_add_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u) (ht : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x ((s + t) x)) u
theorem mdifferentiable_add_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) (ht : MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x ((s + t) x)
theorem mdifferentiableWithinAt_neg_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s : (x : B) โ†’ E x} {u : Set B} {xโ‚€ : B} (hs : MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (-s x)) u xโ‚€
theorem mdifferentiableAt_neg_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s : (x : B) โ†’ E x} {xโ‚€ : B} (hs : MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (-s x)) xโ‚€
theorem mdifferentiableOn_neg_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s : (x : B) โ†’ E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (-s x)) u
theorem mdifferentiable_neg_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s : (x : B) โ†’ E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (-s x)
theorem mdifferentiableWithinAt_sub_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} {u : Set B} {xโ‚€ : B} (hs : MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u xโ‚€) (ht : MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x ((s - t) x)) u xโ‚€
theorem mdifferentiableAt_sub_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} {xโ‚€ : B} (hs : MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) xโ‚€) (ht : MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x ((s - t) x)) xโ‚€
theorem mDifferentiableOn_sub_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u) (ht : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x ((s - t) x)) u
theorem mdifferentiable_sub_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {s t : (x : B) โ†’ E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) (ht : MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (t x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x ((s - t) x)
theorem MDifferentiableWithinAt.smul_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {f : B โ†’ ๐•œ} {s : (x : B) โ†’ E x} {u : Set B} {xโ‚€ : B} (hf : MDifferentiableWithinAt I (modelWithCornersSelf ๐•œ ๐•œ) f u xโ‚€) (hs : MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (f x โ€ข s x)) u xโ‚€
theorem MDifferentiableAt.smul_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {f : B โ†’ ๐•œ} {s : (x : B) โ†’ E x} {xโ‚€ : B} (hf : MDifferentiableAt I (modelWithCornersSelf ๐•œ ๐•œ) f xโ‚€) (hs : MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (f x โ€ข s x)) xโ‚€
theorem MDifferentiableOn.smul_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {f : B โ†’ ๐•œ} {s : (x : B) โ†’ E x} {u : Set B} (hf : MDifferentiableOn I (modelWithCornersSelf ๐•œ ๐•œ) f u) (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (f x โ€ข s x)) u
theorem mdifferentiable_smul_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {f : B โ†’ ๐•œ} {s : (x : B) โ†’ E x} (hf : MDifferentiable I (modelWithCornersSelf ๐•œ ๐•œ) f) (hs : MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (f x โ€ข s x)
theorem mdifferentiableWithinAt_smul_const_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {a : ๐•œ} {s : (x : B) โ†’ E x} {u : Set B} {xโ‚€ : B} (hs : MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (a โ€ข s x)) u xโ‚€
theorem MDifferentiableAt.smul_const_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {a : ๐•œ} {s : (x : B) โ†’ E x} {xโ‚€ : B} (hs : MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (a โ€ข s x)) xโ‚€
theorem MDifferentiableOn.smul_const_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {a : ๐•œ} {s : (x : B) โ†’ E x} {u : Set B} (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (a โ€ข s x)) u
theorem mdifferentiable_smul_const_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {a : ๐•œ} {s : (x : B) โ†’ E x} (hs : MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (a โ€ข s x)
theorem MDifferentiableWithinAt.sum_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {u : Set B} {xโ‚€ : B} {ฮน : Type u_9} {s : Finset ฮน} {t : ฮน โ†’ (x : B) โ†’ E x} (hs : โˆ€ (i : ฮน), MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘ i โˆˆ s, t i x)) u xโ‚€
theorem MDifferentiableAt.sum_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {ฮน : Type u_9} {s : Finset ฮน} {t : ฮน โ†’ (x : B) โ†’ E x} {xโ‚€ : B} (hs : โˆ€ (i : ฮน), MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘ i โˆˆ s, t i x)) xโ‚€
theorem MDifferentiableOn.sum_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {u : Set B} {ฮน : Type u_9} {s : Finset ฮน} {t : ฮน โ†’ (x : B) โ†’ E x} (hs : โˆ€ (i : ฮน), MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘ i โˆˆ s, t i x)) u
theorem MDifferentiable.sum_section {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {ฮน : Type u_9} {s : Finset ฮน} {t : ฮน โ†’ (x : B) โ†’ E x} (hs : โˆ€ (i : ฮน), MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘ i โˆˆ s, t i x)
theorem MDifferentiableOn.smul_section_of_tsupport {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {u : Set B} {s : (x : B) โ†’ E x} {ฯˆ : B โ†’ ๐•œ} (hฯˆ : MDifferentiableOn I (modelWithCornersSelf ๐•œ ๐•œ) ฯˆ u) (ht : IsOpen u) (ht' : tsupport ฯˆ โІ u) (hs : MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (s x)) u) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (ฯˆ x โ€ข s x)

The scalar product ฯˆ โ€ข s of a differentiable function ฯˆ : M โ†’ ๐•œ and a section s of a vector bundle V โ†’ M is differentiable once s is differentiable on an open set containing tsupport ฯˆ.

See ContMDiffOn.smul_section_of_tsupport for the analogous result about C^n sections.

theorem MDifferentiableWithinAt.sum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {u : Set B} {xโ‚€ : B} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘' (i : ฮน), t i x)) u xโ‚€

The sum of a locally finite collection of sections is differentiable if each section is. Version at a point within a set.

theorem MDifferentiableAt.sum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {xโ‚€ : B} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘' (i : ฮน), t i x)) xโ‚€

The sum of a locally finite collection of sections is differentiable at x if each section is.

theorem MDifferentiableOn.sum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {u : Set B} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘' (i : ฮน), t i x)) u

The sum of a locally finite collection of sections is differentiable on a set u if each section is.

theorem MDifferentiable.sum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘' (i : ฮน), t i x)

The sum of a locally finite collection of sections is differentiable if each section is.

theorem MDifferentiableWithinAt.finsum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {u : Set B} {xโ‚€ : B} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) u xโ‚€) :
MDifferentiableWithinAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘แถ  (i : ฮน), t i x)) u xโ‚€
theorem MDifferentiableAt.finsum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {xโ‚€ : B} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) xโ‚€) :
MDifferentiableAt I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘แถ  (i : ฮน), t i x)) xโ‚€
theorem MDifferentiableOn.finsum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {u : Set B} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) u) :
MDifferentiableOn I (I.prod (modelWithCornersSelf ๐•œ F)) (fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘แถ  (i : ฮน), t i x)) u
theorem MDifferentiable.finsum_section_of_locallyFinite {๐•œ : Type u_1} {B : Type u_2} {F : Type u_4} {E : B โ†’ Type u_6} [TopologicalSpace B] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) โ†’ TopologicalSpace (E x)] [NormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NormedSpace ๐•œ F] [FiberBundle F E] [(x : B) โ†’ AddCommGroup (E x)] [(x : B) โ†’ Module ๐•œ (E x)] [VectorBundle ๐•œ F E] {HB : Type u_7} [TopologicalSpace HB] [ChartedSpace HB B] {EB : Type u_8} [NormedAddCommGroup EB] [NormedSpace ๐•œ EB] {I : ModelWithCorners ๐•œ EB HB} {ฮน : Type u_9} {t : ฮน โ†’ (x : B) โ†’ E x} (ht : LocallyFinite fun (i : ฮน) => {x : B | t i x โ‰  0}) (ht' : โˆ€ (i : ฮน), MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (t i x)) :
MDifferentiable I (I.prod (modelWithCornersSelf ๐•œ F)) fun (x : B) => Bundle.TotalSpace.mk' F x (โˆ‘แถ  (i : ฮน), t i x)
theorem MDifferentiableWithinAt.clm_apply_of_inCoordinates {๐•œ : Type u_1} {Fโ‚ : Type u_2} {Fโ‚‚ : Type u_3} {Bโ‚ : Type u_4} {Bโ‚‚ : Type u_5} {M : Type u_6} {Eโ‚ : Bโ‚ โ†’ Type u_7} {Eโ‚‚ : Bโ‚‚ โ†’ Type u_8} [NontriviallyNormedField ๐•œ] [(x : Bโ‚) โ†’ AddCommGroup (Eโ‚ x)] [(x : Bโ‚) โ†’ Module ๐•œ (Eโ‚ x)] [NormedAddCommGroup Fโ‚] [NormedSpace ๐•œ Fโ‚] [TopologicalSpace (Bundle.TotalSpace Fโ‚ Eโ‚)] [(x : Bโ‚) โ†’ TopologicalSpace (Eโ‚ x)] [(x : Bโ‚‚) โ†’ AddCommGroup (Eโ‚‚ x)] [(x : Bโ‚‚) โ†’ Module ๐•œ (Eโ‚‚ x)] [NormedAddCommGroup Fโ‚‚] [NormedSpace ๐•œ Fโ‚‚] [TopologicalSpace (Bundle.TotalSpace Fโ‚‚ Eโ‚‚)] [(x : Bโ‚‚) โ†’ TopologicalSpace (Eโ‚‚ x)] {EBโ‚ : Type u_9} [NormedAddCommGroup EBโ‚] [NormedSpace ๐•œ EBโ‚] {HBโ‚ : Type u_10} [TopologicalSpace HBโ‚] {IBโ‚ : ModelWithCorners ๐•œ EBโ‚ HBโ‚} [TopologicalSpace Bโ‚] [ChartedSpace HBโ‚ Bโ‚] {EBโ‚‚ : Type u_11} [NormedAddCommGroup EBโ‚‚] [NormedSpace ๐•œ EBโ‚‚] {HBโ‚‚ : Type u_12} [TopologicalSpace HBโ‚‚] {IBโ‚‚ : ModelWithCorners ๐•œ EBโ‚‚ HBโ‚‚} [TopologicalSpace Bโ‚‚] [ChartedSpace HBโ‚‚ Bโ‚‚] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace ๐•œ EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners ๐•œ EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle Fโ‚ Eโ‚] [VectorBundle ๐•œ Fโ‚ Eโ‚] [FiberBundle Fโ‚‚ Eโ‚‚] [VectorBundle ๐•œ Fโ‚‚ Eโ‚‚] {bโ‚ : M โ†’ Bโ‚} {bโ‚‚ : M โ†’ Bโ‚‚} {mโ‚€ : M} {ฯ• : (m : M) โ†’ Eโ‚ (bโ‚ m) โ†’L[๐•œ] Eโ‚‚ (bโ‚‚ m)} {v : (m : M) โ†’ Eโ‚ (bโ‚ m)} {s : Set M} (hฯ• : MDifferentiableWithinAt IM (modelWithCornersSelf ๐•œ (Fโ‚ โ†’L[๐•œ] Fโ‚‚)) (fun (m : M) => ContinuousLinearMap.inCoordinates Fโ‚ Eโ‚ Fโ‚‚ Eโ‚‚ (bโ‚ mโ‚€) (bโ‚ m) (bโ‚‚ mโ‚€) (bโ‚‚ m) (ฯ• m)) s mโ‚€) (hv : MDifferentiableWithinAt IM (IBโ‚.prod (modelWithCornersSelf ๐•œ Fโ‚)) (fun (m : M) => { proj := bโ‚ m, snd := v m }) s mโ‚€) (hbโ‚‚ : MDifferentiableWithinAt IM IBโ‚‚ bโ‚‚ s mโ‚€) :
MDifferentiableWithinAt IM (IBโ‚‚.prod (modelWithCornersSelf ๐•œ Fโ‚‚)) (fun (m : M) => { proj := bโ‚‚ m, snd := (ฯ• m) (v m) }) s mโ‚€

Consider a differentiable map v : M โ†’ Eโ‚ to a vector bundle, over a basemap bโ‚ : M โ†’ Bโ‚, and another basemap bโ‚‚ : M โ†’ Bโ‚‚. Given linear maps ฯ• m : Eโ‚ (bโ‚ m) โ†’ Eโ‚‚ (bโ‚‚ m) depending differentiably on m, one can apply ฯ• m to g m, and the resulting map is differentiable.

Note that the differentiability of ฯ• cannot be always be stated as differentiability of a map into a manifold, as the pullback bundles bโ‚ *แต– Eโ‚ and bโ‚‚ *แต– Eโ‚‚ only make sense when bโ‚ and bโ‚‚ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using differentiability of ฯ• read in coordinates.

Version for MDifferentiableWithinAt. We also give a version for MDifferentiableAt, but no version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates, only makes sense around a point.

theorem MDifferentiableAt.clm_apply_of_inCoordinates {๐•œ : Type u_1} {Fโ‚ : Type u_2} {Fโ‚‚ : Type u_3} {Bโ‚ : Type u_4} {Bโ‚‚ : Type u_5} {M : Type u_6} {Eโ‚ : Bโ‚ โ†’ Type u_7} {Eโ‚‚ : Bโ‚‚ โ†’ Type u_8} [NontriviallyNormedField ๐•œ] [(x : Bโ‚) โ†’ AddCommGroup (Eโ‚ x)] [(x : Bโ‚) โ†’ Module ๐•œ (Eโ‚ x)] [NormedAddCommGroup Fโ‚] [NormedSpace ๐•œ Fโ‚] [TopologicalSpace (Bundle.TotalSpace Fโ‚ Eโ‚)] [(x : Bโ‚) โ†’ TopologicalSpace (Eโ‚ x)] [(x : Bโ‚‚) โ†’ AddCommGroup (Eโ‚‚ x)] [(x : Bโ‚‚) โ†’ Module ๐•œ (Eโ‚‚ x)] [NormedAddCommGroup Fโ‚‚] [NormedSpace ๐•œ Fโ‚‚] [TopologicalSpace (Bundle.TotalSpace Fโ‚‚ Eโ‚‚)] [(x : Bโ‚‚) โ†’ TopologicalSpace (Eโ‚‚ x)] {EBโ‚ : Type u_9} [NormedAddCommGroup EBโ‚] [NormedSpace ๐•œ EBโ‚] {HBโ‚ : Type u_10} [TopologicalSpace HBโ‚] {IBโ‚ : ModelWithCorners ๐•œ EBโ‚ HBโ‚} [TopologicalSpace Bโ‚] [ChartedSpace HBโ‚ Bโ‚] {EBโ‚‚ : Type u_11} [NormedAddCommGroup EBโ‚‚] [NormedSpace ๐•œ EBโ‚‚] {HBโ‚‚ : Type u_12} [TopologicalSpace HBโ‚‚] {IBโ‚‚ : ModelWithCorners ๐•œ EBโ‚‚ HBโ‚‚} [TopologicalSpace Bโ‚‚] [ChartedSpace HBโ‚‚ Bโ‚‚] {EM : Type u_13} [NormedAddCommGroup EM] [NormedSpace ๐•œ EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners ๐•œ EM HM} [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle Fโ‚ Eโ‚] [VectorBundle ๐•œ Fโ‚ Eโ‚] [FiberBundle Fโ‚‚ Eโ‚‚] [VectorBundle ๐•œ Fโ‚‚ Eโ‚‚] {bโ‚ : M โ†’ Bโ‚} {bโ‚‚ : M โ†’ Bโ‚‚} {mโ‚€ : M} {ฯ• : (m : M) โ†’ Eโ‚ (bโ‚ m) โ†’L[๐•œ] Eโ‚‚ (bโ‚‚ m)} {v : (m : M) โ†’ Eโ‚ (bโ‚ m)} (hฯ• : MDifferentiableAt IM (modelWithCornersSelf ๐•œ (Fโ‚ โ†’L[๐•œ] Fโ‚‚)) (fun (m : M) => ContinuousLinearMap.inCoordinates Fโ‚ Eโ‚ Fโ‚‚ Eโ‚‚ (bโ‚ mโ‚€) (bโ‚ m) (bโ‚‚ mโ‚€) (bโ‚‚ m) (ฯ• m)) mโ‚€) (hv : MDifferentiableAt IM (IBโ‚.prod (modelWithCornersSelf ๐•œ Fโ‚)) (fun (m : M) => { proj := bโ‚ m, snd := v m }) mโ‚€) (hbโ‚‚ : MDifferentiableAt IM IBโ‚‚ bโ‚‚ mโ‚€) :
MDifferentiableAt IM (IBโ‚‚.prod (modelWithCornersSelf ๐•œ Fโ‚‚)) (fun (m : M) => { proj := bโ‚‚ m, snd := (ฯ• m) (v m) }) mโ‚€

Consider a differentiable map v : M โ†’ Eโ‚ to a vector bundle, over a basemap bโ‚ : M โ†’ Bโ‚, and another basemap bโ‚‚ : M โ†’ Bโ‚‚. Given linear maps ฯ• m : Eโ‚ (bโ‚ m) โ†’ Eโ‚‚ (bโ‚‚ m) depending differentiably on m, one can apply ฯ• m to g m, and the resulting map is differentiable.

Note that the differentiability of ฯ• cannot be always be stated as differentiability of a map into a manifold, as the pullback bundles bโ‚ *แต– Eโ‚ and bโ‚‚ *แต– Eโ‚‚ only make sense when bโ‚ and bโ‚‚ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using differentiability of ฯ• read in coordinates.

Version for MDifferentiableAt. We also give a version for MDifferentiableWithinAt, but no version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates, only makes sense around a point.