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.

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) => Bundle.TotalSpace.mk' F x (self.toFun x)

  proof that this section is C^n

@[deprecated ContMDiffSection (since := "2024-11-21")]

def SmoothSection {𝕜 : 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)

Alias of ContMDiffSection.

---

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

Equations

• @SmoothSection = @ContMDiffSection

def Manifold.«termCₛ^_⟮_;_,_⟯» : Lean.ParserDescr

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.

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) => { 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 : 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) => Bundle.TotalSpace.mk' F x (s x)

@[deprecated ContMDiffSection.contMDiff (since := "2024-11-21")]

theorem ContMDiffSection.smooth {𝕜 : 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) => Bundle.TotalSpace.mk' F x (s x)

Alias of ContMDiffSection.contMDiff.

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) : 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] : Function.Injective DFunLike.coe

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) : 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 : M → Type 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 : 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) : ⇑(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 : 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) : ⇑(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 : 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)

Equations

• ContMDiffSection.instZero = { zero := { toFun := fun (x : M) => 0, contMDiff_toFun := ⋯ } }

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] : ⇑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 : 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) : ⇑(-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 : 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 : ℕ) : ⇑(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 : 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 : ℤ) : ⇑(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 : 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

• ContMDiffSection.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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) : ⇑(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 : 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] : ContMDiffSection I F n V →+ (x : M) → V x

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

Equations

• ContMDiffSection.coeAddHom I F n V = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[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) : (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 : 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

• ContMDiffSection.instModule = Function.Injective.module 𝕜 (ContMDiffSection.coeAddHom I F n V) ⋯ ⋯

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 : 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 : M → Type 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 : M → Type 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