Basic properties of C^n functions between manifolds #
In this file, we show that standard operations on C^n maps between manifolds are C^n :
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 isC^ncontMDiff_isOpenEmbeddingshows that ifMhas aChartedSpacestructure induced by an open embeddinge : M ā H, theneisC^n.
Tags #
chain rule, manifolds, higher derivative
Regularity of the composition of C^n 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 : WithTop ENat}
{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 (Function.comp 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 : WithTop ENat}
{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 : Eq (f x) y)
:
ContMDiffWithinAt I I'' n (Function.comp g f) s x
See note [comp_of_eq lemmas]
@[deprecated ContMDiffWithinAt.comp (since := "2024-11-20")]
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}
{n : WithTop ENat}
{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 (Function.comp g f) s x
Alias of ContMDiffWithinAt.comp.
The composition of C^n functions within domains at points is C^n.
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 : WithTop ENat}
{t : Set M'}
{g : M' ā M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiffOn I I' n f s)
(st : HasSubset.Subset s (Set.preimage f t))
:
ContMDiffOn I I'' n (Function.comp g f) s
The composition of C^n functions on domains is C^n.
@[deprecated ContMDiffOn.comp (since := "2024-11-20")]
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}
{n : WithTop ENat}
{t : Set M'}
{g : M' ā M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiffOn I I' n f s)
(st : HasSubset.Subset s (Set.preimage f t))
:
ContMDiffOn I I'' n (Function.comp g f) s
Alias of ContMDiffOn.comp.
The composition of C^n functions on domains is C^n.
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 : WithTop ENat}
{t : Set M'}
{g : M' ā M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiffOn I I' n f s)
:
ContMDiffOn I I'' n (Function.comp g f) (Inter.inter s (Set.preimage f t))
The composition of C^n functions on domains is C^n.
@[deprecated ContMDiffOn.comp' (since := "2024-11-20")]
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}
{n : WithTop ENat}
{t : Set M'}
{g : M' ā M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiffOn I I' n f s)
:
ContMDiffOn I I'' n (Function.comp g f) (Inter.inter s (Set.preimage f t))
Alias of ContMDiffOn.comp'.
The composition of C^n functions on domains is C^n.
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 : WithTop ENat}
{g : M' ā M''}
(hg : ContMDiff I' I'' n g)
(hf : ContMDiff I I' n f)
:
ContMDiff I I'' n (Function.comp g f)
The composition of C^n functions is C^n.
@[deprecated ContMDiff.comp (since := "2024-11-20")]
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'}
{n : WithTop ENat}
{g : M' ā M''}
(hg : ContMDiff I' I'' n g)
(hf : ContMDiff I I' n f)
:
ContMDiff I I'' n (Function.comp g f)
Alias of ContMDiff.comp.
The composition of C^n functions is C^n.
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 : WithTop ENat}
{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 (Function.comp g f) (Inter.inter s (Set.preimage f t)) x
The composition of C^n functions within domains at points is C^n.
@[deprecated ContMDiffWithinAt.comp' (since := "2024-11-20")]
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}
{n : WithTop ENat}
{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 (Function.comp g f) (Inter.inter s (Set.preimage f t)) x
Alias of ContMDiffWithinAt.comp'.
The composition of C^n functions within domains at points is C^n.
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 : WithTop ENat}
{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 (Function.comp 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.
@[deprecated ContMDiffAt.comp_contMDiffWithinAt (since := "2024-11-20")]
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}
{n : WithTop ENat}
{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 (Function.comp g f) s x
Alias of ContMDiffAt.comp_contMDiffWithinAt.
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
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 : WithTop ENat}
{g : M' ā M''}
(x : M)
(hg : ContMDiffAt I' I'' n g (f x))
(hf : ContMDiffAt I I' n f x)
:
ContMDiffAt I I'' n (Function.comp 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 : WithTop ENat}
{g : M' ā M''}
{x : M}
{y : M'}
(hg : ContMDiffAt I' I'' n g y)
(hf : ContMDiffAt I I' n f x)
(hx : Eq (f x) y)
:
ContMDiffAt I I'' n (Function.comp g f) x
See note [comp_of_eq lemmas]
@[deprecated ContMDiffAt.comp (since := "2024-11-20")]
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'}
{n : WithTop ENat}
{g : M' ā M''}
(x : M)
(hg : ContMDiffAt I' I'' n g (f x))
(hf : ContMDiffAt I I' n f x)
:
ContMDiffAt I I'' n (Function.comp g f) x
Alias of ContMDiffAt.comp.
The composition of C^n functions at points is C^n.
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 : WithTop ENat}
{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 (Function.comp g f) s
@[deprecated ContMDiff.comp_contMDiffOn (since := "2024-11-20")]
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'']
{n : WithTop ENat}
{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 (Function.comp g f) s
Alias of ContMDiff.comp_contMDiffOn.
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 : WithTop ENat}
{t : Set M'}
{g : M' ā M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiff I I' n f)
(ht : ā (x : M), Membership.mem t (f x))
:
ContMDiff I I'' n (Function.comp g f)
@[deprecated ContMDiffOn.comp_contMDiff (since := "2024-11-20")]
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'}
{n : WithTop ENat}
{t : Set M'}
{g : M' ā M''}
(hg : ContMDiffOn I' I'' n g t)
(hf : ContMDiff I I' n f)
(ht : ā (x : M), Membership.mem t (f x))
:
ContMDiff I I'' n (Function.comp g f)
Alias of ContMDiffOn.comp_contMDiff.
The identity is C^n #
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 : WithTop ENat}
:
@[deprecated contMDiff_id (since := "2024-11-20")]
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]
{n : WithTop ENat}
:
Alias of contMDiff_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 : WithTop ENat}
:
ContMDiffOn I I n id s
@[deprecated contMDiffOn_id (since := "2024-11-20")]
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}
{n : WithTop ENat}
:
ContMDiffOn I I n id s
Alias of contMDiffOn_id.
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 : WithTop ENat}
:
ContMDiffAt I I n id x
@[deprecated contMDiffAt_id (since := "2024-11-20")]
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}
{n : WithTop ENat}
:
ContMDiffAt I I n id x
Alias of contMDiffAt_id.
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 : WithTop ENat}
:
ContMDiffWithinAt I I n id s x
@[deprecated contMDiffWithinAt_id (since := "2024-11-20")]
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}
{n : WithTop ENat}
:
ContMDiffWithinAt I I n id s x
Alias of contMDiffWithinAt_id.
Constants are C^n #
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 : WithTop ENat}
{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 : WithTop ENat}
[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 : WithTop ENat}
[Zero M']
:
ContMDiff I I' n 0
@[deprecated contMDiff_const (since := "2024-11-20")]
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']
{n : WithTop ENat}
{c : M'}
:
ContMDiff I I' n fun (x : M) => c
Alias of contMDiff_const.
@[deprecated contMDiff_one (since := "2024-11-20")]
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']
{n : WithTop ENat}
[One M']
:
ContMDiff I I' n 1
Alias of contMDiff_one.
@[deprecated contMDiff_zero (since := "2024-11-20")]
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']
{n : WithTop ENat}
[Zero M']
:
ContMDiff I I' n 0
Alias of contMDiff_zero.
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 : WithTop ENat}
{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 : WithTop ENat}
[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 : WithTop ENat}
[Zero M']
:
ContMDiffOn I I' n 0 s
@[deprecated contMDiffOn_const (since := "2024-11-20")]
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}
{n : WithTop ENat}
{c : M'}
:
ContMDiffOn I I' n (fun (x : M) => c) s
Alias of contMDiffOn_const.
@[deprecated contMDiffOn_one (since := "2024-11-20")]
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}
{n : WithTop ENat}
[One M']
:
ContMDiffOn I I' n 1 s
Alias of contMDiffOn_one.
@[deprecated contMDiffOn_zero (since := "2024-11-20")]
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}
{n : WithTop ENat}
[Zero M']
:
ContMDiffOn I I' n 0 s
Alias of contMDiffOn_zero.
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 : WithTop ENat}
{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 : WithTop ENat}
[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 : WithTop ENat}
[Zero M']
:
ContMDiffAt I I' n 0 x
@[deprecated contMDiffAt_const (since := "2024-11-20")]
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}
{n : WithTop ENat}
{c : M'}
:
ContMDiffAt I I' n (fun (x : M) => c) x
Alias of contMDiffAt_const.
@[deprecated contMDiffAt_one (since := "2024-11-20")]
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}
{n : WithTop ENat}
[One M']
:
ContMDiffAt I I' n 1 x
Alias of contMDiffAt_one.
@[deprecated contMDiffAt_zero (since := "2024-11-20")]
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}
{n : WithTop ENat}
[Zero M']
:
ContMDiffAt I I' n 0 x
Alias of contMDiffAt_zero.
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 : WithTop ENat}
{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 : WithTop ENat}
[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 : WithTop ENat}
[Zero M']
:
ContMDiffWithinAt I I' n 0 s x
@[deprecated contMDiffWithinAt_const (since := "2024-11-20")]
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}
{n : WithTop ENat}
{c : M'}
:
ContMDiffWithinAt I I' n (fun (x : M) => c) s x
Alias of contMDiffWithinAt_const.
@[deprecated contMDiffWithinAt_one (since := "2024-11-20")]
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}
{n : WithTop ENat}
[One M']
:
ContMDiffWithinAt I I' n 1 s x
Alias of contMDiffWithinAt_one.
@[deprecated contMDiffWithinAt_zero (since := "2024-11-20")]
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}
{n : WithTop ENat}
[Zero M']
:
ContMDiffWithinAt I I' n 0 s x
Alias of contMDiffWithinAt_zero.
theorem
contMDiff_of_subsingleton
{š : 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'}
{n : WithTop ENat}
[Subsingleton M']
:
ContMDiff I I' n f
theorem
contMDiffAt_of_subsingleton
{š : 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'}
{x : M}
{n : WithTop ENat}
[Subsingleton M']
:
ContMDiffAt I I' n f x
theorem
contMDiffWithinAt_of_subsingleton
{š : 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'}
{s : Set M}
{x : M}
{n : WithTop ENat}
[Subsingleton M']
:
ContMDiffWithinAt I I' n f s x
theorem
contMDiffOn_of_subsingleton
{š : 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'}
{s : Set M}
{n : WithTop ENat}
[Subsingleton M']
:
ContMDiffOn I I' n f s
theorem
contMDiff_of_discreteTopology
{š : 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'}
{n : WithTop ENat}
[DiscreteTopology M]
:
ContMDiff I I' n f
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 : WithTop ENat}
[One M']
{f : M ā M'}
(hf : ā (x : M), Membership.mem (mulTSupport f) x ā 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 : WithTop ENat}
[Zero M']
{f : M ā M'}
(hf : ā (x : M), Membership.mem (tsupport f) x ā 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 : Not (Membership.mem (mulTSupport f) x))
(n : WithTop ENat)
(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 : Not (Membership.mem (tsupport f) x))
(n : WithTop ENat)
(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 : Not (Membership.mem (mulTSupport f) x))
(n : WithTop ENat)
:
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 : Not (Membership.mem (tsupport f) x))
(n : WithTop ENat)
:
ContMDiffAt I I' n f x
The inclusion map from one open set to another is C^n #
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 : WithTop ENat}
{U : TopologicalSpace.Opens M}
{f : M ā M'}
{x : Subtype fun (x : M) => Membership.mem U x}
:
Iff (ContMDiffAt I I' n (fun (x : Subtype fun (x : M) => Membership.mem U x) => f x.val) x) (ContMDiffAt I I' n f x.val)
@[deprecated contMDiffAt_subtype_iff (since := "2024-11-20")]
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 : WithTop ENat}
{U : TopologicalSpace.Opens M}
{f : M ā M'}
{x : Subtype fun (x : M) => Membership.mem U x}
:
Iff (ContMDiffAt I I' n (fun (x : Subtype fun (x : M) => Membership.mem U x) => f x.val) x) (ContMDiffAt I I' n f x.val)
Alias of contMDiffAt_subtype_iff.
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 : WithTop ENat}
{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 : WithTop ENat}
{U : TopologicalSpace.Opens M}
{f : (Subtype fun (x : M) => Membership.mem U x) ā 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 : WithTop ENat}
{U : TopologicalSpace.Opens M}
{f : (Subtype fun (x : M) => Membership.mem U x) ā 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 : WithTop ENat}
{U V : TopologicalSpace.Opens M}
(h : LE.le U V)
:
ContMDiff I I n (TopologicalSpace.Opens.inclusion h)
@[deprecated contMDiffAt_subtype_iff (since := "2024-11-20")]
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']
{n : WithTop ENat}
{U : TopologicalSpace.Opens M}
{f : M ā M'}
{x : Subtype fun (x : M) => Membership.mem U x}
:
Iff (ContMDiffAt I I' n (fun (x : Subtype fun (x : M) => Membership.mem U x) => f x.val) x) (ContMDiffAt I I' n f x.val)
Alias of contMDiffAt_subtype_iff.
@[deprecated contMDiff_subtype_val (since := "2024-11-20")]
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]
{n : WithTop ENat}
{U : TopologicalSpace.Opens M}
:
ContMDiff I I n Subtype.val
Alias of contMDiff_subtype_val.
@[deprecated ContMDiff.extend_one (since := "2024-11-20")]
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']
{n : WithTop ENat}
{U : TopologicalSpace.Opens M}
{f : (Subtype fun (x : M) => Membership.mem U x) ā M'}
(supp : HasCompactMulSupport f)
(diff : ContMDiff I I' n f)
:
ContMDiff I I' n (Function.extend Subtype.val f 1)
Alias of ContMDiff.extend_one.
@[deprecated ContMDiff.extend_zero (since := "2024-11-20")]
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']
{n : WithTop ENat}
{U : TopologicalSpace.Opens M}
{f : (Subtype fun (x : M) => Membership.mem U x) ā M'}
(supp : HasCompactSupport f)
(diff : ContMDiff I I' n f)
:
ContMDiff I I' n (Function.extend Subtype.val f 0)
Alias of ContMDiff.extend_zero.
@[deprecated contMDiff_inclusion (since := "2024-11-20")]
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]
{n : WithTop ENat}
{U V : TopologicalSpace.Opens M}
(h : LE.le U V)
:
ContMDiff I I n (TopologicalSpace.Opens.inclusion h)
Alias of contMDiff_inclusion.
Open embeddings and their inverses are C^n #
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 ENat}
[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 C^n.
@[deprecated contMDiff_isOpenEmbedding (since := "2024-10-18")]
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 ENat}
[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 C^n.
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 ENat}
[Nonempty M]
:
ContMDiffOn I I n (Topology.IsOpenEmbedding.toPartialHomeomorph e h).symm.toFun' (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 C^n.
@[deprecated contMDiffOn_isOpenEmbedding_symm (since := "2024-10-18")]
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 ENat}
[Nonempty M]
:
ContMDiffOn I I n (Topology.IsOpenEmbedding.toPartialHomeomorph e h).symm.toFun' (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 C^n.
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 ENat}
[ChartedSpace H M]
[Nonempty M']
{e' : M' ā H'}
(h' : Topology.IsOpenEmbedding e')
{f : M ā M'}
(hf : ContMDiff I I' n (Function.comp 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'. If e' ā f : M ā H' is C^n, then f is C^n.
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 (since := "2024-10-18")]
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 ENat}
[ChartedSpace H M]
[Nonempty M']
{e' : M' ā H'}
(h' : Topology.IsOpenEmbedding e')
{f : M ā M'}
(hf : ContMDiff I I' n (Function.comp 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'. If e' ā f : M ā H' is C^n, then f is C^n.
This is useful, for example, when e' ā f = g ā e for smooth maps e : M ā X and g : X ā H'.