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_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 : ℕ∞)
(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.
- 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
Instances For
theorem
ContMDiffSection.contMDiff_toFun
{𝕜 : 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 : ℕ∞}
{V : M → Type u_6}
[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_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]
:
Type (max u_4 u_6)
Bundled smooth sections of a vector bundle.
Equations
- SmoothSection I F V = ContMDiffSection I F ⊤ V
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_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 : ℕ∞}
{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 : ℕ∞}
{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 : ℕ∞}
{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)
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]
{V : M → Type u_6}
[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_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 : ℕ∞}
{V : M → Type u_6}
[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_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 : ℕ∞}
{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_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 : ℕ∞}
{V : M → Type u_6}
[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}
:
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 : ℕ∞}
{V : M → Type u_6}
[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_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 : ℕ∞}
{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 : ℕ∞}
{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)
(t : ContMDiffSection I F n V)
:
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 : ℕ∞}
{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 : ℕ∞}
{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)
(t : ContMDiffSection I F n V)
:
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 : ℕ∞}
{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 : ℕ∞}
{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 : ℕ∞}
{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 : ℕ∞}
{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 : ℕ∞}
{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
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 : ℕ∞}
{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 : ℕ∞}
{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
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 : ℕ∞}
{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 : ℕ∞}
{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
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 : ℕ∞}
{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 : ℕ∞}
{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 : ℕ∞}
{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 : ℕ∞)
(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 smooth sections to dependent maps.
Equations
- ContMDiffSection.coeAddHom I F n V = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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 : ℕ∞}
{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 : ℕ∞}
{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