Documentation

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

C^n sections #

In this file we define the type ContMDiffSection of n times continuously differentiable sections of a vector bundle over a manifold M and prove that it's a module over the base field.

In passing, we prove that binary and finite sums, differences and scalar products of C^n sections are C^n.

theorem ContMDiffWithinAt.add_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M} {x₀ : M} (hs : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u x₀) (ht : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) u x₀) :
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x ((s + t) x)) u x₀
theorem ContMDiffAt.add_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {x₀ : M} (hs : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) x₀) (ht : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) x₀) :
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x ((s + t) x)) x₀
theorem ContMDiffOn.add_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M} (hs : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u) (ht : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) u) :
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x ((s + t) x)) u
theorem ContMDiff.add_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} (hs : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) (ht : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) :
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x ((s + t) x)
theorem ContMDiffWithinAt.neg_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} {u : Set M} {x₀ : M} (hs : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u x₀) :
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (-s x)) u x₀
theorem ContMDiffAt.neg_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} {x₀ : M} (hs : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) x₀) :
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (-s x)) x₀
theorem ContMDiffOn.neg_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} {u : Set M} (hs : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u) :
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (-s x)) u
theorem ContMDiff.neg_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} (hs : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) :
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (-s x)
theorem ContMDiffWithinAt.sub_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M} {x₀ : M} (hs : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u x₀) (ht : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) u x₀) :
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x ((s - t) x)) u x₀
theorem ContMDiffAt.sub_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {x₀ : M} (hs : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) x₀) (ht : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) x₀) :
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x ((s - t) x)) x₀
theorem ContMDiffOn.sub_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M} (hs : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u) (ht : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) u) :
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x ((s - t) x)) u
theorem ContMDiff.sub_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} (hs : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) (ht : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (t x)) :
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x ((s - t) x)
theorem ContMDiffWithinAt.smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M𝕜} {s : (x : M) → V x} {u : Set M} {x₀ : M} (hf : ContMDiffWithinAt I (modelWithCornersSelf 𝕜 𝕜) n f u x₀) (hs : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u x₀) :
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (f x s x)) u x₀
theorem ContMDiffAt.smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M𝕜} {s : (x : M) → V x} {x₀ : M} (hf : ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) n f x₀) (hs : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) x₀) :
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (f x s x)) x₀
theorem ContMDiffOn.smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M𝕜} {s : (x : M) → V x} {u : Set M} (hf : ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n f u) (hs : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u) :
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (f x s x)) u
theorem ContMDiff.smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M𝕜} {s : (x : M) → V x} (hf : ContMDiff I (modelWithCornersSelf 𝕜 𝕜) n f) (hs : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) :
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (f x s x)
theorem ContMDiffWithinAt.const_smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {a : 𝕜} {s : (x : M) → V x} {u : Set M} {x₀ : M} (hs : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u x₀) :
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (a s x)) u x₀
theorem ContMDiffAt.const_smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {a : 𝕜} {s : (x : M) → V x} {x₀ : M} (hs : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) x₀) :
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (a s x)) x₀
theorem ContMDiffOn.const_smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {a : 𝕜} {s : (x : M) → V x} {u : Set M} (hs : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u) :
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (a s x)) u
theorem ContMDiff.const_smul_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {a : 𝕜} {s : (x : M) → V x} (hs : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) :
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (a s x)
theorem ContMDiffWithinAt.sum_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {x₀ : M} {ι : Type u_7} {s : Finset ι} {t : ι(x : M) → V x} (hs : is, ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t i x)) u x₀) :
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (∑ is, t i x)) u x₀
theorem ContMDiffAt.sum_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {ι : Type u_7} {s : Finset ι} {t : ι(x : M) → V x} {x₀ : M} (hs : is, ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t i x)) x₀) :
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (∑ is, t i x)) x₀
theorem ContMDiffOn.sum_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {ι : Type u_7} {s : Finset ι} {t : ι(x : M) → V x} (hs : is, ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (t i x)) u) :
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (∑ is, t i x)) u
theorem ContMDiff.sum_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {ι : Type u_7} {s : Finset ι} {t : ι(x : M) → V x} (hs : is, ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (t i x)) :
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (∑ is, t i x)
theorem ContMDiffOn.smul_section_of_tsupport {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s : (x : M) → V x} {ψ : M𝕜} {u : Set M} ( : ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n ψ u) (ht : IsOpen u) (ht' : tsupport ψ u) (hs : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) u) :
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (ψ x s x)

The scalar product ψ • s of a C^k function ψ : M → 𝕜 and a section s of a vector bundle V → M is C^k once s is C^k on an open set containing tsupport ψ .

This is a vector bundle analogue of contMDiff_of_tsupport.

structure ContMDiffSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (V : MType u_6) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
Type (max u_4 u_6)

Bundled n times continuously differentiable sections of a vector bundle. Denoted as Cₛ^n⟮I; F, V⟯ within the Manifold namespace.

Instances For

    Bundled n times continuously differentiable sections of a vector bundle. Denoted as Cₛ^n⟮I; F, V⟯ within the Manifold namespace.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance ContMDiffSection.instDFunLike {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
      Equations
      @[simp]
      theorem ContMDiffSection.coeFn_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] (s : (x : M) → V x) (hs : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => { proj := x, snd := s x }) :
      { toFun := s, contMDiff_toFun := hs } = s
      theorem ContMDiffSection.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] (s : ContMDiffSection I F n V) :
      ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => Bundle.TotalSpace.mk' F x (s x)
      theorem ContMDiffSection.coe_inj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] s t : ContMDiffSection I F n V (h : s = t) :
      s = t
      theorem ContMDiffSection.coe_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
      theorem ContMDiffSection.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {s t : ContMDiffSection I F n V} (h : ∀ (x : M), s x = t x) :
      s = t
      theorem ContMDiffSection.ext_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {s t : ContMDiffSection I F n V} :
      s = t ∀ (x : M), s x = t x
      instance ContMDiffSection.instAdd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      @[simp]
      theorem ContMDiffSection.coe_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s t : ContMDiffSection I F n V) :
      ⇑(s + t) = s + t
      instance ContMDiffSection.instSub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      @[simp]
      theorem ContMDiffSection.coe_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s t : ContMDiffSection I F n V) :
      ⇑(s - t) = s - t
      instance ContMDiffSection.instZero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      instance ContMDiffSection.inhabited {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      @[simp]
      theorem ContMDiffSection.coe_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      0 = 0
      instance ContMDiffSection.instNeg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      @[simp]
      theorem ContMDiffSection.coe_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) :
      ⇑(-s) = -s
      instance ContMDiffSection.instNSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      @[simp]
      theorem ContMDiffSection.coe_nsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (k : ) :
      ⇑(k s) = k s
      instance ContMDiffSection.instZSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      @[simp]
      theorem ContMDiffSection.coe_zsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (z : ) :
      ⇑(z s) = z s
      instance ContMDiffSection.instAddCommGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      Equations
      instance ContMDiffSection.instSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      SMul 𝕜 (ContMDiffSection I F n V)
      Equations
      @[simp]
      theorem ContMDiffSection.coe_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (r : 𝕜) (s : ContMDiffSection I F n V) :
      ⇑(r s) = r s
      def ContMDiffSection.coeAddHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (V : MType u_6) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
      ContMDiffSection I F n V →+ (x : M) → V x

      The additive morphism from C^n sections to dependent maps.

      Equations
      Instances For
        @[simp]
        theorem ContMDiffSection.coeAddHom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) :
        (coeAddHom I F n V) s = s
        instance ContMDiffSection.instModule {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] :
        Module 𝕜 (ContMDiffSection I F n V)
        Equations
        theorem ContMDiffSection.mdifferentiable' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] (s : ContMDiffSection I F n V) (hn : 1 n) :
        MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : M) => Bundle.TotalSpace.mk' F x (s x)
        theorem ContMDiffSection.mdifferentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] (s : ContMDiffSection I F (↑) V) :
        MDifferentiable I (I.prod (modelWithCornersSelf 𝕜 F)) fun (x : M) => Bundle.TotalSpace.mk' F x (s x)
        theorem ContMDiffSection.mdifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : MType u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] (s : ContMDiffSection I F (↑) V) {x : M} :
        MDifferentiableAt I (I.prod (modelWithCornersSelf 𝕜 F)) (fun (x : M) => Bundle.TotalSpace.mk' F x (s x)) x