Basic properties of smooth functions between manifolds #
In this file, we show that standard operations on smooth maps between smooth manifolds are smooth:
ContMDiffOn.compgives the invariance of theCโฟproperty under compositioncontMDiff_idgives the smoothness of the identitycontMDiff_constgives the smoothness of constant functionscontMDiff_inclusionshows that the inclusion between open sets of a topological space is smoothcontMDiff_isOpenEmbeddingshows that ifMhas aChartedSpacestructure induced by an open embeddinge : M โ H, theneis smooth.
Tags #
chain rule, manifolds, higher derivative
Smoothness of the composition of smooth functions between manifolds #
theorem
ContMDiffWithinAt.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{n : โโ}
{t : Set M'}
{g : M' โ M''}
(x : M)
(hg : ContMDiffWithinAt I' I'' n g t (f x))
(hf : ContMDiffWithinAt I I' n f s x)
(st : Set.MapsTo f s t)
:
ContMDiffWithinAt I I'' n (g โ f) s x
The composition of C^n functions within domains at points is C^n.
theorem
ContMDiffWithinAt.comp_of_eq
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{n : โโ}
{t : Set M'}
{g : M' โ M''}
{x : M}
{y : M'}
(hg : ContMDiffWithinAt I' I'' n g t y)
(hf : ContMDiffWithinAt I I' n f s x)
(st : Set.MapsTo f s t)
(hx : f x = y)
:
ContMDiffWithinAt I I'' n (g โ f) s x
See note [comp_of_eq lemmas]
theorem
SmoothWithinAt.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{t : Set M'}
{g : M' โ M''}
(x : M)
(hg : SmoothWithinAt I' I'' g t (f x))
(hf : SmoothWithinAt I I' f s x)
(st : Set.MapsTo f s t)
:
SmoothWithinAt I I'' (g โ f) s x
The composition of C^โ functions within domains at points is C^โ.
theorem
ContMDiffOn.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{n : โโ}
{t : Set M'}
{g : M' โ M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiffOn I I' n f s)
(st : s โ f โปยน' t)
:
ContMDiffOn I I'' n (g โ f) s
The composition of C^n functions on domains is C^n.
theorem
SmoothOn.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{t : Set M'}
{g : M' โ M''}
(hg : SmoothOn I' I'' g t)
(hf : SmoothOn I I' f s)
(st : s โ f โปยน' t)
:
The composition of C^โ functions on domains is C^โ.
theorem
ContMDiffOn.comp'
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{n : โโ}
{t : Set M'}
{g : M' โ M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiffOn I I' n f s)
:
ContMDiffOn I I'' n (g โ f) (s โฉ f โปยน' t)
The composition of C^n functions on domains is C^n.
theorem
SmoothOn.comp'
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{t : Set M'}
{g : M' โ M''}
(hg : SmoothOn I' I'' g t)
(hf : SmoothOn I I' f s)
:
The composition of C^โ functions is C^โ.
theorem
ContMDiff.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{n : โโ}
{g : M' โ M''}
(hg : ContMDiff I' I'' n g)
(hf : ContMDiff I I' n f)
:
The composition of C^n functions is C^n.
theorem
Smooth.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{g : M' โ M''}
(hg : Smooth I' I'' g)
(hf : Smooth I I' f)
:
The composition of C^โ functions is C^โ.
theorem
ContMDiffWithinAt.comp'
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{n : โโ}
{t : Set M'}
{g : M' โ M''}
(x : M)
(hg : ContMDiffWithinAt I' I'' n g t (f x))
(hf : ContMDiffWithinAt I I' n f s x)
:
ContMDiffWithinAt I I'' n (g โ f) (s โฉ f โปยน' t) x
The composition of C^n functions within domains at points is C^n.
theorem
SmoothWithinAt.comp'
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{t : Set M'}
{g : M' โ M''}
(x : M)
(hg : SmoothWithinAt I' I'' g t (f x))
(hf : SmoothWithinAt I I' f s x)
:
SmoothWithinAt I I'' (g โ f) (s โฉ f โปยน' t) x
The composition of C^โ functions within domains at points is C^โ.
theorem
ContMDiffAt.comp_contMDiffWithinAt
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{n : โโ}
{g : M' โ M''}
(x : M)
(hg : ContMDiffAt I' I'' n g (f x))
(hf : ContMDiffWithinAt I I' n f s x)
:
ContMDiffWithinAt I I'' n (g โ f) s x
g โ f is C^n within s at x if g is C^n at f x and
f is C^n within s at x.
theorem
SmoothAt.comp_smoothWithinAt
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{s : Set M}
{g : M' โ M''}
(x : M)
(hg : SmoothAt I' I'' g (f x))
(hf : SmoothWithinAt I I' f s x)
:
SmoothWithinAt I I'' (g โ f) s x
g โ f is C^โ within s at x if g is C^โ at f x and
f is C^โ within s at x.
theorem
ContMDiffAt.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{n : โโ}
{g : M' โ M''}
(x : M)
(hg : ContMDiffAt I' I'' n g (f x))
(hf : ContMDiffAt I I' n f x)
:
ContMDiffAt I I'' n (g โ f) x
The composition of C^n functions at points is C^n.
theorem
ContMDiffAt.comp_of_eq
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{n : โโ}
{g : M' โ M''}
{x : M}
{y : M'}
(hg : ContMDiffAt I' I'' n g y)
(hf : ContMDiffAt I I' n f x)
(hx : f x = y)
:
ContMDiffAt I I'' n (g โ f) x
See note [comp_of_eq lemmas]
theorem
SmoothAt.comp
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{g : M' โ M''}
(x : M)
(hg : SmoothAt I' I'' g (f x))
(hf : SmoothAt I I' f x)
:
The composition of C^โ functions at points is C^โ.
theorem
ContMDiff.comp_contMDiffOn
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{n : โโ}
{f : M โ M'}
{g : M' โ M''}
{s : Set M}
(hg : ContMDiff I' I'' n g)
(hf : ContMDiffOn I I' n f s)
:
ContMDiffOn I I'' n (g โ f) s
theorem
Smooth.comp_smoothOn
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{g : M' โ M''}
{s : Set M}
(hg : Smooth I' I'' g)
(hf : SmoothOn I I' f s)
:
theorem
ContMDiffOn.comp_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{n : โโ}
{t : Set M'}
{g : M' โ M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiff I I' n f)
(ht : โ (x : M), f x โ t)
:
theorem
SmoothOn.comp_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace 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]
[ChartedSpace H' M']
[ChartedSpace H'' M'']
{f : M โ M'}
{t : Set M'}
{g : M' โ M''}
(hg : SmoothOn I' I'' g t)
(hf : Smooth I I' f)
(ht : โ (x : M), f x โ t)
:
The identity is smooth #
theorem
contMDiff_id
{๐ : 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]
{n : โโ}
:
ContMDiff I I n id
theorem
smooth_id
{๐ : 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]
:
Smooth I I id
theorem
contMDiffOn_id
{๐ : 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]
{s : Set M}
{n : โโ}
:
ContMDiffOn I I n id s
theorem
smoothOn_id
{๐ : 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]
{s : Set M}
:
SmoothOn I I id s
theorem
contMDiffAt_id
{๐ : 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]
{x : M}
{n : โโ}
:
ContMDiffAt I I n id x
theorem
smoothAt_id
{๐ : 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]
{x : M}
:
SmoothAt I I id x
theorem
contMDiffWithinAt_id
{๐ : 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]
{s : Set M}
{x : M}
{n : โโ}
:
ContMDiffWithinAt I I n id s x
theorem
smoothWithinAt_id
{๐ : 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]
{s : Set M}
{x : M}
:
SmoothWithinAt I I id s x
Constants are smooth #
theorem
contMDiff_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{n : โโ}
{c : M'}
:
ContMDiff I I' n fun (x : M) => c
theorem
contMDiff_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{n : โโ}
[One M']
:
ContMDiff I I' n 1
theorem
contMDiff_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{n : โโ}
[Zero M']
:
ContMDiff I I' n 0
theorem
smooth_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{c : M'}
:
Smooth I I' fun (x : M) => c
theorem
smooth_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
[One M']
:
Smooth I I' 1
theorem
smooth_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
[Zero M']
:
Smooth I I' 0
theorem
contMDiffOn_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{n : โโ}
{c : M'}
:
ContMDiffOn I I' n (fun (x : M) => c) s
theorem
contMDiffOn_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{n : โโ}
[One M']
:
ContMDiffOn I I' n 1 s
theorem
contMDiffOn_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{n : โโ}
[Zero M']
:
ContMDiffOn I I' n 0 s
theorem
smoothOn_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{c : M'}
:
SmoothOn I I' (fun (x : M) => c) s
theorem
smoothOn_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
[One M']
:
SmoothOn I I' 1 s
theorem
smoothOn_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
[Zero M']
:
SmoothOn I I' 0 s
theorem
contMDiffAt_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{x : M}
{n : โโ}
{c : M'}
:
ContMDiffAt I I' n (fun (x : M) => c) x
theorem
contMDiffAt_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{x : M}
{n : โโ}
[One M']
:
ContMDiffAt I I' n 1 x
theorem
contMDiffAt_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{x : M}
{n : โโ}
[Zero M']
:
ContMDiffAt I I' n 0 x
theorem
smoothAt_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{x : M}
{c : M'}
:
SmoothAt I I' (fun (x : M) => c) x
theorem
smoothAt_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{x : M}
[One M']
:
SmoothAt I I' 1 x
theorem
smoothAt_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{x : M}
[Zero M']
:
SmoothAt I I' 0 x
theorem
contMDiffWithinAt_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{x : M}
{n : โโ}
{c : M'}
:
ContMDiffWithinAt I I' n (fun (x : M) => c) s x
theorem
contMDiffWithinAt_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{x : M}
{n : โโ}
[One M']
:
ContMDiffWithinAt I I' n 1 s x
theorem
contMDiffWithinAt_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{x : M}
{n : โโ}
[Zero M']
:
ContMDiffWithinAt I I' n 0 s x
theorem
smoothWithinAt_const
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{x : M}
{c : M'}
:
SmoothWithinAt I I' (fun (x : M) => c) s x
theorem
smoothWithinAt_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{x : M}
[One M']
:
SmoothWithinAt I I' 1 s x
theorem
smoothWithinAt_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{s : Set M}
{x : M}
[Zero M']
:
SmoothWithinAt I I' 0 s x
theorem
contMDiff_of_mulTSupport
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{n : โโ}
[One M']
{f : M โ M'}
(hf : โ x โ mulTSupport f, ContMDiffAt I I' n f x)
:
ContMDiff I I' n f
f is continuously differentiable if it is cont. differentiable at
each x โ mulTSupport f.
theorem
contMDiff_of_tsupport
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{n : โโ}
[Zero M']
{f : M โ M'}
(hf : โ x โ tsupport f, ContMDiffAt I I' n f x)
:
ContMDiff I I' n f
f is continuously differentiable if it is continuously
differentiable at each x โ tsupport f.
theorem
contMDiffWithinAt_of_not_mem_mulTSupport
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{f : M โ M'}
[One M']
{x : M}
(hx : x โ mulTSupport f)
(n : โโ)
(s : Set M)
:
ContMDiffWithinAt I I' n f s x
theorem
contMDiffWithinAt_of_not_mem
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{f : M โ M'}
[Zero M']
{x : M}
(hx : x โ tsupport f)
(n : โโ)
(s : Set M)
:
ContMDiffWithinAt I I' n f s x
theorem
contMDiffAt_of_not_mem_mulTSupport
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{f : M โ M'}
[One M']
{x : M}
(hx : x โ mulTSupport f)
(n : โโ)
:
ContMDiffAt I I' n f x
f is continuously differentiable at each point outside of its mulTSupport.
theorem
contMDiffAt_of_not_mem
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{f : M โ M'}
[Zero M']
{x : M}
(hx : x โ tsupport f)
(n : โโ)
:
ContMDiffAt I I' n f x
The inclusion map from one open set to another is smooth #
theorem
contMdiffAt_subtype_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{n : โโ}
{U : TopologicalSpace.Opens M}
{f : M โ M'}
{x : โฅU}
:
ContMDiffAt I I' n (fun (x : โฅU) => f โx) x โ ContMDiffAt I I' n f โx
theorem
contMDiff_subtype_val
{๐ : 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]
{n : โโ}
{U : TopologicalSpace.Opens M}
:
ContMDiff I I n Subtype.val
theorem
ContMDiff.extend_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
[T2Space M]
[One M']
{n : โโ}
{U : TopologicalSpace.Opens M}
{f : โฅU โ M'}
(supp : HasCompactMulSupport f)
(diff : ContMDiff I I' n f)
:
ContMDiff I I' n (Function.extend Subtype.val f 1)
theorem
ContMDiff.extend_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
[T2Space M]
[Zero M']
{n : โโ}
{U : TopologicalSpace.Opens M}
{f : โฅU โ M'}
(supp : HasCompactSupport f)
(diff : ContMDiff I I' n f)
:
ContMDiff I I' n (Function.extend Subtype.val f 0)
theorem
contMDiff_inclusion
{๐ : 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]
{n : โโ}
{U V : TopologicalSpace.Opens M}
(h : U โค V)
:
ContMDiff I I n (TopologicalSpace.Opens.inclusion h)
theorem
smooth_subtype_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
{U : TopologicalSpace.Opens M}
{f : M โ M'}
{x : โฅU}
:
theorem
smooth_subtype_val
{๐ : 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]
{U : TopologicalSpace.Opens M}
:
Smooth I I Subtype.val
theorem
Smooth.extend_one
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
[T2Space M]
[One M']
{U : TopologicalSpace.Opens M}
{f : โฅU โ M'}
(supp : HasCompactMulSupport f)
(diff : Smooth I I' f)
:
Smooth I I' (Function.extend Subtype.val f 1)
theorem
Smooth.extend_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H M]
[ChartedSpace H' M']
[T2Space M]
[Zero M']
{U : TopologicalSpace.Opens M}
{f : โฅU โ M'}
(supp : HasCompactSupport f)
(diff : Smooth I I' f)
:
Smooth I I' (Function.extend Subtype.val f 0)
theorem
smooth_inclusion
{๐ : 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]
{U V : TopologicalSpace.Opens M}
(h : U โค V)
:
Open embeddings and their inverses are smooth #
theorem
contMDiff_isOpenEmbedding
{๐ : 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]
{e : M โ H}
(h : Topology.IsOpenEmbedding e)
{n : WithTop โ}
[Nonempty M]
:
ContMDiff I I n e
If the ChartedSpace structure on a manifold M is given by an open embedding e : M โ H,
then e is smooth.
@[deprecated contMDiff_isOpenEmbedding]
theorem
contMDiff_openEmbedding
{๐ : 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]
{e : M โ H}
(h : Topology.IsOpenEmbedding e)
{n : WithTop โ}
[Nonempty M]
:
ContMDiff I I n e
Alias of contMDiff_isOpenEmbedding.
If the ChartedSpace structure on a manifold M is given by an open embedding e : M โ H,
then e is smooth.
theorem
contMDiffOn_isOpenEmbedding_symm
{๐ : 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]
{e : M โ H}
(h : Topology.IsOpenEmbedding e)
{n : WithTop โ}
[Nonempty M]
:
ContMDiffOn I I n (โ(Topology.IsOpenEmbedding.toPartialHomeomorph e h).symm) (Set.range e)
If the ChartedSpace structure on a manifold M is given by an open embedding e : M โ H,
then the inverse of e is smooth.
@[deprecated contMDiffOn_isOpenEmbedding_symm]
theorem
contMDiffOn_openEmbedding_symm
{๐ : 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]
{e : M โ H}
(h : Topology.IsOpenEmbedding e)
{n : WithTop โ}
[Nonempty M]
:
ContMDiffOn I I n (โ(Topology.IsOpenEmbedding.toPartialHomeomorph e h).symm) (Set.range e)
Alias of contMDiffOn_isOpenEmbedding_symm.
If the ChartedSpace structure on a manifold M is given by an open embedding e : M โ H,
then the inverse of e is smooth.
theorem
ContMDiff.of_comp_isOpenEmbedding
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
{n : WithTop โ}
[ChartedSpace H M]
[Nonempty M']
{e' : M' โ H'}
(h' : Topology.IsOpenEmbedding e')
{f : M โ M'}
(hf : ContMDiff I I' n (e' โ f))
:
ContMDiff I I' n f
Let M' be a manifold whose chart structure is given by an open embedding e' into its model
space H'. Then the smoothness of e' โ f : M โ H' implies the smoothness of f.
This is useful, for example, when e' โ f = g โ e for smooth maps e : M โ X and g : X โ H'.
@[deprecated ContMDiff.of_comp_isOpenEmbedding]
theorem
ContMDiff.of_comp_openEmbedding
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
{n : WithTop โ}
[ChartedSpace H M]
[Nonempty M']
{e' : M' โ H'}
(h' : Topology.IsOpenEmbedding e')
{f : M โ M'}
(hf : ContMDiff I I' n (e' โ f))
:
ContMDiff I I' n f
Alias of ContMDiff.of_comp_isOpenEmbedding.
Let M' be a manifold whose chart structure is given by an open embedding e' into its model
space H'. Then the smoothness of e' โ f : M โ H' implies the smoothness of f.
This is useful, for example, when e' โ f = g โ e for smooth maps e : M โ X and g : X โ H'.