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
.
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
.
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
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
Equations
- ContMDiffSection.instDFunLike = { coe := ContMDiffSection.toFun, coe_injective' := ⋯ }
Equations
- ContMDiffSection.instAdd = { add := fun (s t : ContMDiffSection I F n V) => { toFun := ⇑s + ⇑t, contMDiff_toFun := ⋯ } }
Equations
- ContMDiffSection.instSub = { sub := fun (s t : ContMDiffSection I F n V) => { toFun := ⇑s - ⇑t, contMDiff_toFun := ⋯ } }
Equations
- ContMDiffSection.inhabited = { default := 0 }
Equations
- ContMDiffSection.instNeg = { neg := fun (s : ContMDiffSection I F n V) => { toFun := -⇑s, contMDiff_toFun := ⋯ } }
Equations
- ContMDiffSection.instNSMul = { smul := nsmulRec }
Equations
- ContMDiffSection.instZSMul = { smul := zsmulRec }
Equations
Equations
- ContMDiffSection.instSMul = { smul := fun (c : 𝕜) (s : ContMDiffSection I F n V) => { toFun := c • ⇑s, contMDiff_toFun := ⋯ } }
The additive morphism from C^n
sections to dependent maps.
Equations
- ContMDiffSection.coeAddHom I F n V = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }