Documentation

Mathlib.Geometry.Manifold.ContMDiff.Basic

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 :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

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) :

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} :
@[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} :

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} :
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) :
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) :
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) :
@[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} :

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) :

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) :

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) :

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] :

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] :

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'.