Documentation

Mathlib.Geometry.Manifold.ContMDiff.Basic

Basic properties of smooth functions between manifolds #

In this file, we show that standard operations on smooth maps between smooth manifolds are 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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {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) :
SmoothOn I I'' (g โˆ˜ f) s

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] [ChartedSpace H 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'] {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''] {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) :

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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {f : M โ†’ M'} {n : โ„•โˆž} {g : M' โ†’ M''} (hg : ContMDiff I' I'' n g) (hf : ContMDiff I I' n f) :
ContMDiff I I'' n (g โˆ˜ 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] [ChartedSpace H 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'] {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''] {f : M โ†’ M'} {g : M' โ†’ M''} (hg : Smooth I' I'' g) (hf : Smooth I I' f) :
Smooth I I'' (g โˆ˜ 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] [ChartedSpace H 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'] {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''] {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) :

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] [ChartedSpace H 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'] {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''] {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) :

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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {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] [ChartedSpace H 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'] {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''] {f : M โ†’ M'} {g : M' โ†’ M''} (x : M) (hg : SmoothAt I' I'' g (f x)) (hf : SmoothAt I I' f x) :
SmoothAt I I'' (g โˆ˜ 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] [ChartedSpace H 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'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] {n : โ„•โˆž} {f : 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] [ChartedSpace H 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'] {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''] {f : M โ†’ M'} {g : M' โ†’ M''} {s : Set M} (hg : Smooth I' I'' g) (hf : SmoothOn I I' f s) :
SmoothOn I I'' (g โˆ˜ 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] [ChartedSpace H 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'] {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''] {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) :
ContMDiff I I'' n (g โˆ˜ f)
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] [ChartedSpace H 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'] {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''] {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) :
Smooth I I'' (g โˆ˜ f)

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] [ChartedSpace H 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'] {n : โ„•โˆž} {c : M'} :
ContMDiff I I' n fun (x : M) => c
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] [ChartedSpace H 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'] {n : โ„•โˆž} [Zero M'] :
ContMDiff I I' n 0
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] [ChartedSpace H 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'] {n : โ„•โˆž} [One M'] :
ContMDiff I I' n 1
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] [ChartedSpace H 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'] {c : M'} :
Smooth I I' fun (x : M) => c
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] [ChartedSpace H 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'] [Zero M'] :
Smooth I I' 0
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] [ChartedSpace H 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'] [One M'] :
Smooth I I' 1
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] [ChartedSpace H 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'] {s : Set M} {n : โ„•โˆž} {c : M'} :
ContMDiffOn I I' n (fun (x : M) => c) 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] [ChartedSpace H 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'] {s : Set M} {n : โ„•โˆž} [Zero M'] :
ContMDiffOn I I' n 0 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] [ChartedSpace H 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'] {s : Set M} {n : โ„•โˆž} [One M'] :
ContMDiffOn I I' n 1 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] [ChartedSpace H 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'] {s : Set M} {c : M'} :
SmoothOn I I' (fun (x : M) => c) 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] [ChartedSpace H 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'] {s : Set M} [Zero M'] :
SmoothOn I I' 0 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] [ChartedSpace H 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'] {s : Set M} [One M'] :
SmoothOn I I' 1 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] [ChartedSpace H 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'] {x : M} {n : โ„•โˆž} {c : M'} :
ContMDiffAt I I' n (fun (x : M) => c) 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] [ChartedSpace H 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'] {x : M} {n : โ„•โˆž} [Zero M'] :
ContMDiffAt I I' n 0 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] [ChartedSpace H 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'] {x : M} {n : โ„•โˆž} [One M'] :
ContMDiffAt I I' n 1 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] [ChartedSpace H 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'] {x : M} {c : M'} :
SmoothAt I I' (fun (x : M) => c) 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] [ChartedSpace H 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'] {x : M} [Zero M'] :
SmoothAt I I' 0 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] [ChartedSpace H 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'] {x : M} [One M'] :
SmoothAt I I' 1 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] [ChartedSpace H 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'] {s : Set M} {x : M} {n : โ„•โˆž} {c : M'} :
ContMDiffWithinAt I I' n (fun (x : M) => c) 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] [ChartedSpace H 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'] {s : Set M} {x : M} {n : โ„•โˆž} [Zero M'] :
ContMDiffWithinAt I I' n 0 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] [ChartedSpace H 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'] {s : Set M} {x : M} {n : โ„•โˆž} [One M'] :
ContMDiffWithinAt I I' n 1 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] [ChartedSpace H 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'] {s : Set M} {x : M} {c : M'} :
SmoothWithinAt I I' (fun (x : M) => c) 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] [ChartedSpace H 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'] {s : Set M} {x : M} [Zero M'] :
SmoothWithinAt I I' 0 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] [ChartedSpace H 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'] {s : Set M} {x : M} [One M'] :
SmoothWithinAt I I' 1 s x
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] [ChartedSpace H 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'] {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 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] [ChartedSpace H 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'] {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.

@[deprecated contMDiff_of_tsupport]
theorem contMDiff_of_support {๐•œ : 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] {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'] {n : โ„•โˆž} [Zero M'] {f : M โ†’ M'} (hf : โˆ€ x โˆˆ tsupport f, ContMDiffAt I I' n f x) :
ContMDiff I I' n f

Alias of contMDiff_of_tsupport.


f is continuously differentiable if it is continuously differentiable at each x โˆˆ tsupport f.

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] [ChartedSpace H 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'] {f : M โ†’ M'} [Zero M'] {x : M} (hx : x โˆ‰ tsupport f) (n : โ„•โˆž) (s : Set M) :
ContMDiffWithinAt I I' n f s x
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] [ChartedSpace H 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'] {f : M โ†’ M'} [One M'] {x : M} (hx : x โˆ‰ mulTSupport f) (n : โ„•โˆž) (s : Set M) :
ContMDiffWithinAt I I' n f s x
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] [ChartedSpace H 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'] {f : M โ†’ M'} [Zero M'] {x : M} (hx : x โˆ‰ tsupport f) (n : โ„•โˆž) :
ContMDiffAt I I' n f 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] [ChartedSpace H 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'] {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.

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] [ChartedSpace H 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'] {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_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] [ChartedSpace H 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'] [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.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] [ChartedSpace H 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'] [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_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 : TopologicalSpace.Opens M} {V : TopologicalSpace.Opens M} (h : U โ‰ค V) :
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] [ChartedSpace H 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'] {U : TopologicalSpace.Opens M} {f : M โ†’ M'} {x : โ†ฅU} :
SmoothAt I I' (fun (x : โ†ฅU) => f โ†‘x) x โ†” SmoothAt I I' f โ†‘x
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_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] [ChartedSpace H 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'] [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.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] [ChartedSpace H 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'] [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_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 : TopologicalSpace.Opens M} {V : TopologicalSpace.Opens M} (h : U โ‰ค V) :

Open embeddings and their inverses are smooth #

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] [Nonempty M] {e : M โ†’ H} (h : OpenEmbedding e) {n : WithTop โ„•} :
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.

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] [Nonempty M] {e : M โ†’ H} (h : OpenEmbedding e) {n : WithTop โ„•} :

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_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] [ChartedSpace H 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'] [Nonempty M] [Nonempty M'] {e' : M' โ†’ H'} (h' : OpenEmbedding e') {n : WithTop โ„•} {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'.