C^n bundled maps #
In this file we define the type ContMDiffMap of n times continuously differentiable
bundled maps.
def
ContMDiffMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
(I : ModelWithCorners 𝕜 E H)
(I' : ModelWithCorners 𝕜 E' H')
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
(M' : Type u_7)
[TopologicalSpace M']
[ChartedSpace H' M']
(n : WithTop ℕ∞)
:
Type (max 0 u_6 u_7)
Bundled n times continuously differentiable maps,
denoted as C^n(I, M; I', M') and C^n(I, M; k) (when the target is a normed space k with
the trivial model) in the Manifold namespace.
@[deprecated ContMDiffMap (since := "2024-11-21")]
def
SmoothMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
(I : ModelWithCorners 𝕜 E H)
(I' : ModelWithCorners 𝕜 E' H')
(M : Type u_6)
[TopologicalSpace M]
[ChartedSpace H M]
(M' : Type u_7)
[TopologicalSpace M']
[ChartedSpace H' M']
(n : WithTop ℕ∞)
:
Type (max 0 u_6 u_7)
Alias of ContMDiffMap.
Bundled n times continuously differentiable maps,
denoted as C^n(I, M; I', M') and C^n(I, M; k) (when the target is a normed space k with
the trivial model) in the Manifold namespace.
Equations
Bundled n times continuously differentiable maps,
denoted as C^n(I, M; I', M') and C^n(I, M; k) (when the target is a normed space k with
the trivial model) in the Manifold namespace.
Equations
- One or more equations did not get rendered due to their size.
Bundled n times continuously differentiable maps,
denoted as C^n(I, M; I', M') and C^n(I, M; k) (when the target is a normed space k with
the trivial model) in the Manifold namespace.
Equations
- One or more equations did not get rendered due to their size.
instance
ContMDiffMap.instFunLike
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
:
FunLike (ContMDiffMap I I' M M' n) M M'
Equations
- ContMDiffMap.instFunLike = { coe := Subtype.val, coe_injective' := ⋯ }
theorem
ContMDiffMap.contMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
(f : ContMDiffMap I I' M M' n)
:
ContMDiff I I' n ⇑f
@[deprecated ContMDiffMap.contMDiff (since := "2024-11-20")]
theorem
ContMDiffMap.smooth
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
(f : ContMDiffMap I I' M M' n)
:
ContMDiff I I' n ⇑f
Alias of ContMDiffMap.contMDiff.
@[simp]
theorem
ContMDiffMap.coeFn_mk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
(f : M → M')
(hf : ContMDiff I I' n f)
:
theorem
ContMDiffMap.coe_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
⦃f g : ContMDiffMap I I' M M' n⦄
(h : ⇑f = ⇑g)
:
theorem
ContMDiffMap.ext
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
{f g : ContMDiffMap I I' M M' n}
(h : ∀ (x : M), f x = g x)
:
theorem
ContMDiffMap.ext_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
{f g : ContMDiffMap I I' M M' n}
:
instance
ContMDiffMap.instContinuousMapClass
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
:
ContinuousMapClass (ContMDiffMap I I' M M' n) M M'
def
ContMDiffMap.id
{𝕜 : 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]
{n : WithTop ℕ∞}
:
ContMDiffMap I I M M n
The identity as a C^n map.
Equations
- ContMDiffMap.id = ⟨id, ⋯⟩
def
ContMDiffMap.comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{n : WithTop ℕ∞}
(f : ContMDiffMap I' I'' M' M'' n)
(g : ContMDiffMap I I' M M' n)
:
ContMDiffMap I I'' M M'' n
The composition of C^n maps, as a C^n map.
@[simp]
theorem
ContMDiffMap.comp_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{n : WithTop ℕ∞}
(f : ContMDiffMap I' I'' M' M'' n)
(g : ContMDiffMap I I' M M' n)
(x : M)
:
instance
ContMDiffMap.instInhabited
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
[Inhabited M']
:
Inhabited (ContMDiffMap I I' M M' n)
def
ContMDiffMap.const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
(y : M')
:
ContMDiffMap I I' M M' n
Constant map as a C^n map
Equations
- ContMDiffMap.const y = ⟨fun (x : M) => y, ⋯⟩
def
ContMDiffMap.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
:
ContMDiffMap (I.prod I') I (M × M') M n
The first projection of a product, as a C^n map.
Equations
def
ContMDiffMap.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : WithTop ℕ∞}
:
ContMDiffMap (I.prod I') I' (M × M') M' n
The second projection of a product, as a C^n map.
Equations
def
ContMDiffMap.prodMk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_4}
[TopologicalSpace H]
{H' : Type u_5}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{I' : ModelWithCorners 𝕜 E' H'}
{M : Type u_6}
[TopologicalSpace M]
[ChartedSpace H M]
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{F : Type u_11}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_12}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_13}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
(f : ContMDiffMap J I N M n)
(g : ContMDiffMap J I' N M' n)
:
ContMDiffMap J (I.prod I') N (M × M') n
Given two C^n maps f and g, this is the C^n map x ↦ (f x, g x).
instance
ContinuousLinearMap.hasCoeToContMDiffMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(n : WithTop ℕ∞)
:
Coe (E →L[𝕜] E') (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n)