Documentation

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

Smooth sections #

In this file we define the type ContMDiffSection of n times continuously differentiable sections of a smooth 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_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_11) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ∞) (V : MType u_12) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
Type (max u_12 u_6)

Bundled n times continuously differentiable sections of a vector bundle.

Instances For
    theorem ContMDiffSection.contMDiff_toFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] (self : ContMDiffSection I F n V) :
    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

    @[reducible, inline]
    abbrev SmoothSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_11) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : MType u_12) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
    Type (max u_12 u_6)

    Bundled smooth sections of a vector bundle.

    Equations
    Instances For

      Bundled n times continuously differentiable sections of a vector bundle.

      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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F 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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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.smooth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : MType u_12} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] (s : ContMDiffSection I F V) :
        Smooth I (I.prod (modelWithCornersSelf 𝕜 F)) 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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] ⦃s : ContMDiffSection I F n V ⦃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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
        Function.Injective DFunLike.coe
        theorem ContMDiffSection.ext_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {s : ContMDiffSection I F n V} {t : ContMDiffSection I F n V} :
        s = t ∀ (x : M), s x = t x
        theorem ContMDiffSection.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] {s : ContMDiffSection I F n V} {t : ContMDiffSection I F n V} (h : ∀ (x : M), s x = t x) :
        s = t
        instance ContMDiffSection.instAdd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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
        • 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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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) (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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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
        • 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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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) (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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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
        • 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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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
        • ContMDiffSection.inhabited = { default := 0 }
        @[simp]
        theorem ContMDiffSection.coe_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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
        • 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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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
        • ContMDiffSection.instNSMul = { smul := nsmulRec }
        @[simp]
        theorem ContMDiffSection.coe_nsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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
        • ContMDiffSection.instZSMul = { smul := zsmulRec }
        @[simp]
        theorem ContMDiffSection.coe_zsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_11) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ∞) (V : MType u_12) [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 smooth sections to dependent maps.

        Equations
        Instances For
          instance ContMDiffSection.instModule {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : MType u_12} [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_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : MType u_12} [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