Smooth bundled map #
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 : ℕ∞)
:
Type (max 0 u_6 u_7)
Bundled n times continuously differentiable maps.
Instances For
@[reducible]
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']
:
Type (max 0 u_6 u_7)
Bundled smooth maps.
Instances For
instance
ContMDiffMap.funLike
{𝕜 : 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 : ℕ∞}
:
FunLike (ContMDiffMap I I' M M' n) M fun x => M'
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 : ℕ∞}
(f : ContMDiffMap I I' M M' n)
:
ContMDiff I I' n ↑f
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']
(f : ContMDiffMap I I' M M' ⊤)
:
Smooth I I' ↑f
@[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 : ℕ∞}
(f : M → M')
(hf : ContMDiff I I' n f)
:
↑{ val := f, property := hf } = 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 : ℕ∞}
⦃f : ContMDiffMap I I' M M' n⦄
⦃g : ContMDiffMap I I' M M' n⦄
(h : ↑f = ↑g)
:
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 : ℕ∞}
{f : ContMDiffMap I I' M M' n}
{g : ContMDiffMap I I' M M' n}
(h : ∀ (x : M), ↑f x = ↑g x)
:
f = g
instance
ContMDiffMap.instContinuousMapClassContMDiffMap
{𝕜 : 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 : ℕ∞}
:
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 : ℕ∞}
:
ContMDiffMap I I M M n
The identity as a smooth map.
Instances For
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 : ℕ∞}
(f : ContMDiffMap I' I'' M' M'' n)
(g : ContMDiffMap I I' M M' n)
:
ContMDiffMap I I'' M M'' n
The composition of smooth maps, as a smooth map.
Instances For
@[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 : ℕ∞}
(f : ContMDiffMap I' I'' M' M'' n)
(g : ContMDiffMap I I' M M' n)
(x : M)
:
↑(ContMDiffMap.comp f g) x = ↑f (↑g x)
instance
ContMDiffMap.instInhabitedContMDiffMap
{𝕜 : 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 : ℕ∞}
[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 : ℕ∞}
(y : M')
:
ContMDiffMap I I' M M' n
Constant map as a smooth map
Instances For
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 : ℕ∞}
:
ContMDiffMap (ModelWithCorners.prod I I') I (M × M') M n
The first projection of a product, as a smooth map.
Instances For
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 : ℕ∞}
:
ContMDiffMap (ModelWithCorners.prod I I') I' (M × M') M' n
The second projection of a product, as a smooth map.
Instances For
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 : ℕ∞}
(f : ContMDiffMap J I N M n)
(g : ContMDiffMap J I' N M' n)
:
ContMDiffMap J (ModelWithCorners.prod I I') N (M × M') n
Given two smooth maps f and g, this is the smooth map x ↦ (f x, g x).
Instances For
instance
ContinuousLinearMap.hasCoeToContMDiffMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(n : ℕ∞)
:
Coe (E →L[𝕜] E') (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n)