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 : M → Type 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) => ⟨x, s x⟩) u x₀)
(ht : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) x₀)
(ht : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) u)
(ht : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩)
(ht : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, t x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) u x₀)
(ht : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) x₀)
(ht : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) u)
(ht : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩)
(ht : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, t x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, (f • 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 : M → Type 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) => ⟨x, s x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, (f • 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 : M → Type 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) => ⟨x, s x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, (f • 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 : M → Type 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) => ⟨x, s x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, (f • 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 : M → Type 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) => ⟨x, s x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨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 : M → Type 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) => ⟨x, s x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨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 : M → Type 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}
{t : ι → (x : M) → V x}
{s : Finset ι}
(hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑ i ∈ s, 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 : M → Type 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]
{x₀ : M}
{ι : Type u_7}
{t : ι → (x : M) → V x}
{s : Finset ι}
(hs : ∀ i ∈ s, ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑ i ∈ s, 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 : M → Type 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}
{t : ι → (x : M) → V x}
{s : Finset ι}
(hs : ∀ i ∈ s, ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑ i ∈ s, 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 : M → Type 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}
{t : ι → (x : M) → V x}
{s : Finset ι}
(hs : ∀ i ∈ s, ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, t i x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, ∑ i ∈ s, 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 : M → Type 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}
{s : (x : M) → V x}
{ψ : M → 𝕜}
(hψ : ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n ψ u)
(ht : IsOpen u)
(ht' : tsupport ψ ⊆ u)
(hs : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, s x⟩) u)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨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.
theorem
ContMDiffWithinAt.sum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑' (i : ι), t i x⟩) u x₀
The sum of a locally finite collection of sections is C^k iff each section is.
Version at a point within a set.
theorem
ContMDiffAt.sum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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]
{x₀ : M}
{ι : Type u_7}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑' (i : ι), t i x⟩) x₀
The sum of a locally finite collection of sections is C^k at x iff each section is.
theorem
ContMDiffOn.sum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑' (i : ι), t i x⟩) u
The sum of a locally finite collection of sections is C^k on a set u iff each section is.
theorem
ContMDiff.sum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, t i x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, ∑' (i : ι), t i x⟩
The sum of a locally finite collection of sections is C^k iff each section is.
theorem
ContMDiffWithinAt.finsum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) u x₀)
:
ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑ᶠ (i : ι), t i x⟩) u x₀
theorem
ContMDiffAt.finsum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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]
{x₀ : M}
{ι : Type u_7}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) x₀)
:
ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
theorem
ContMDiffOn.finsum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, t i x⟩) u)
:
ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun (x : M) => ⟨x, ∑ᶠ (i : ι), t i x⟩) u
theorem
ContMDiff.finsum_section_of_locallyFinite
{𝕜 : 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 : M → Type 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}
{t : ι → (x : M) → V x}
(ht : LocallyFinite fun (i : ι) => {x : M | t i x ≠ 0})
(ht' : ∀ (i : ι), ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, t i x⟩)
:
ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, ∑ᶠ (i : ι), t i x⟩
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 : M → Type 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.
- toFun (x : M) : V x
the underlying function of this section
- contMDiff_toFun : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, self.toFun x⟩
proof that this section is
C^n
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_reducible]
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 : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
:
DFunLike (ContMDiffSection I F n V) M V
Equations
- ContMDiffSection.instDFunLike = { coe := ContMDiffSection.toFun, coe_injective := ⋯ }
@[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 : M → Type 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) => ⟨x, s x⟩)
:
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 : M → Type 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) => ⟨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 : M → Type 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)
:
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 : M → Type 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 : M → Type 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)
:
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 : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
{s t : ContMDiffSection I F n V}
:
@[instance_reducible]
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 : M → Type 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]
:
Add (ContMDiffSection I F n V)
Equations
- ContMDiffSection.instAdd = { add := fun (s t : ContMDiffSection I F n V) => { toFun := ⇑s + ⇑t, contMDiff_toFun := ⋯ } }
@[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 : M → Type 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)
:
@[instance_reducible]
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 : M → Type 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]
:
Sub (ContMDiffSection I F n V)
Equations
- ContMDiffSection.instSub = { sub := fun (s t : ContMDiffSection I F n V) => { toFun := ⇑s - ⇑t, contMDiff_toFun := ⋯ } }
@[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 : M → Type 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)
:
@[instance_reducible]
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 : M → Type 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]
:
Zero (ContMDiffSection I F n V)
@[instance_reducible]
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 : M → Type 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]
:
Inhabited (ContMDiffSection I F n V)
Equations
- ContMDiffSection.inhabited = { default := 0 }
@[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 : M → Type 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]
:
@[instance_reducible]
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 : M → Type 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]
:
Neg (ContMDiffSection I F n V)
Equations
- ContMDiffSection.instNeg = { neg := fun (s : ContMDiffSection I F n V) => { toFun := -⇑s, contMDiff_toFun := ⋯ } }
@[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 : M → Type 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)
:
@[instance_reducible]
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 : M → Type 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
- ContMDiffSection.instNSMul = { smul := nsmulRec }
@[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 : M → Type 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 : ℕ)
:
@[instance_reducible]
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 : M → Type 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
- ContMDiffSection.instZSMul = { smul := zsmulRec }
@[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 : M → Type 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 : ℤ)
:
@[instance_reducible]
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 : M → Type 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]
:
AddCommGroup (ContMDiffSection I F n V)
Equations
@[instance_reducible]
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 : M → Type 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
- ContMDiffSection.instSMul = { smul := fun (c : 𝕜) (s : ContMDiffSection I F n V) => { toFun := c • ⇑s, contMDiff_toFun := ⋯ } }
@[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 : M → Type 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)
:
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 : M → Type 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]
:
The additive morphism from C^n sections to dependent maps.
Equations
- ContMDiffSection.coeAddHom I F n V = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
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 : M → Type 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)
:
@[instance_reducible]
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 : M → Type 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 : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F n V)
(hn : n ≠ 0)
:
MDiff fun (x : M) => ⟨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 : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F (↑⊤) V)
:
MDiff fun (x : M) => ⟨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 : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F (↑⊤) V)
{x : M}
:
(MDiffAt fun (x : M) => ⟨x, s x⟩) x