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 โ„•โˆž} {t : Set M'} {g : M' โ†’ M''} (x : M) (hg : ContMDiffWithinAt I' I'' n g t (f x)) (hf : ContMDiffWithinAt I I' n f s x) (st : Set.MapsTo f s t) :
ContMDiffWithinAt I I'' n (g โˆ˜ f) s x

The composition of C^n functions within domains at points is C^n.

theorem ContMDiffWithinAt.comp_of_eq {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H M] [ChartedSpace H' M'] [ChartedSpace H'' M''] {f : M โ†’ M'} {s : Set M} {n : WithTop โ„•โˆž} {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 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 โ„•โˆž} {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 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 โ„•โˆž} {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 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 โ„•โˆž} {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 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 โ„•โˆž} {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 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 โ„•โˆž} {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 ContMDiffAt.comp_contMDiffWithinAt_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 โ„•โˆž} {g : M' โ†’ M''} {x : M} {y : M'} (hg : ContMDiffAt I' I'' n g y) (hf : ContMDiffWithinAt I I' n f s x) (hx : f x = y) :
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 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 โ„•โˆž} {g : M' โ†’ M''} (x : M) (hg : ContMDiffAt I' I'' n g (f x)) (hf : ContMDiffAt I I' n f x) :
ContMDiffAt I I'' n (g โˆ˜ f) x

The composition of C^n functions at points is C^n.

theorem ContMDiffAt.comp_of_eq {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace ๐•œ E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners ๐•œ E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H M] [ChartedSpace H' M'] [ChartedSpace H'' M''] {f : M โ†’ M'} {n : WithTop โ„•โˆž} {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 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 โ„•โˆž} {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 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 โ„•โˆž} {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)

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 โ„•โˆž} :
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 โ„•โˆž} :
ContMDiffOn I I n 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 : WithTop โ„•โˆž} :
ContMDiffAt I I n 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 : WithTop โ„•โˆž} :

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 โ„•โˆž} {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 โ„•โˆž} [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 โ„•โˆž} [Zero M'] :
ContMDiff I I' n 0
theorem contMDiffOn_const {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {s : Set M} {n : WithTop โ„•โˆž} {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 โ„•โˆž} [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 โ„•โˆž} [Zero M'] :
ContMDiffOn I I' n 0 s
theorem contMDiffAt_const {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {x : M} {n : WithTop โ„•โˆž} {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 โ„•โˆž} [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 โ„•โˆž} [Zero M'] :
ContMDiffAt I I' n 0 x
theorem contMDiffWithinAt_const {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {s : Set M} {x : M} {n : WithTop โ„•โˆž} {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 โ„•โˆž} [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 โ„•โˆž} [Zero M'] :
ContMDiffWithinAt I I' n 0 s x
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 โ„•โˆž} [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 โ„•โˆž} [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 โ„•โˆž} [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 โ„•โˆž} [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 โ„•โˆž} [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 โ„•โˆž} [One M'] {f : M โ†’ M'} (hf : โˆ€ x โˆˆ mulTSupport f, ContMDiffAt I I' n f x) :
ContMDiff I I' n f

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

theorem contMDiff_of_tsupport {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {n : WithTop โ„•โˆž} [Zero M'] {f : M โ†’ M'} (hf : โˆ€ x โˆˆ tsupport f, ContMDiffAt I I' n f x) :
ContMDiff I I' n f

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

theorem contMDiffWithinAt_of_notMem_mulTSupport {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [One M'] {x : M} (hx : x โˆ‰ mulTSupport f) (n : WithTop โ„•โˆž) (s : Set M) :
ContMDiffWithinAt I I' n f s x
theorem contMDiffWithinAt_of_notMem {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [Zero M'] {x : M} (hx : x โˆ‰ tsupport f) (n : WithTop โ„•โˆž) (s : Set M) :
ContMDiffWithinAt I I' n f s x
@[deprecated contMDiffWithinAt_of_notMem (since := "2025-05-23")]
theorem contMDiffWithinAt_of_not_mem {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [Zero M'] {x : M} (hx : x โˆ‰ tsupport f) (n : WithTop โ„•โˆž) (s : Set M) :
ContMDiffWithinAt I I' n f s x

Alias of contMDiffWithinAt_of_notMem.

@[deprecated contMDiffWithinAt_of_notMem_mulTSupport (since := "2025-05-23")]
theorem contMDiffWithinAt_of_not_mem_mulTSupport {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [One M'] {x : M} (hx : x โˆ‰ mulTSupport f) (n : WithTop โ„•โˆž) (s : Set M) :
ContMDiffWithinAt I I' n f s x

Alias of contMDiffWithinAt_of_notMem_mulTSupport.

theorem contMDiffAt_of_notMem_mulTSupport {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [One M'] {x : M} (hx : x โˆ‰ mulTSupport f) (n : WithTop โ„•โˆž) :
ContMDiffAt I I' n f x

f is continuously differentiable at each point outside of its mulTSupport.

theorem contMDiffAt_of_notMem {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [Zero M'] {x : M} (hx : x โˆ‰ tsupport f) (n : WithTop โ„•โˆž) :
ContMDiffAt I I' n f x
@[deprecated contMDiffAt_of_notMem (since := "2025-05-23")]
theorem contMDiffAt_of_not_mem {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [Zero M'] {x : M} (hx : x โˆ‰ tsupport f) (n : WithTop โ„•โˆž) :
ContMDiffAt I I' n f x

Alias of contMDiffAt_of_notMem.

@[deprecated contMDiffAt_of_notMem_mulTSupport (since := "2025-05-23")]
theorem contMDiffAt_of_not_mem_mulTSupport {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace ๐•œ E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners ๐•œ E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {f : M โ†’ M'} [One M'] {x : M} (hx : x โˆ‰ mulTSupport f) (n : WithTop โ„•โˆž) :
ContMDiffAt I I' n f x

Alias of contMDiffAt_of_notMem_mulTSupport.


f is continuously differentiable at each point outside of its mulTSupport.

Being C^k on a union of open sets can be tested on each set #

theorem ContMDiffOn.union_of_isOpen {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {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 โ„•โˆž} {s t : Set M} (hf : ContMDiffOn I I' n f s) (hf' : ContMDiffOn I I' n f t) (hs : IsOpen s) (ht : IsOpen t) :
ContMDiffOn I I' n f (s โˆช t)

If a function is C^k on two open sets, it is also C^n on their union.

theorem contMDiffOn_union_iff_of_isOpen {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {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 โ„•โˆž} {s t : Set M} (hs : IsOpen s) (ht : IsOpen t) :
ContMDiffOn I I' n f (s โˆช t) โ†” ContMDiffOn I I' n f s โˆง ContMDiffOn I I' n f t

A function is C^k on two open sets iff it is C^k on their union.

theorem contMDiff_of_contMDiffOn_union_of_isOpen {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {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 โ„•โˆž} {s t : Set M} (hf : ContMDiffOn I I' n f s) (hf' : ContMDiffOn I I' n f t) (hst : s โˆช t = Set.univ) (hs : IsOpen s) (ht : IsOpen t) :
ContMDiff I I' n f
theorem ContMDiffOn.iUnion_of_isOpen {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {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 โ„•โˆž} {ฮน : Type u_11} {s : ฮน โ†’ Set M} (hf : โˆ€ (i : ฮน), ContMDiffOn I I' n f (s i)) (hs : โˆ€ (i : ฮน), IsOpen (s i)) :
ContMDiffOn I I' n f (โ‹ƒ (i : ฮน), s i)

If a function is C^k on open sets s i, it is C^k on their union

theorem contMDiffOn_iUnion_iff_of_isOpen {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {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 โ„•โˆž} {ฮน : Type u_11} {s : ฮน โ†’ Set M} (hs : โˆ€ (i : ฮน), IsOpen (s i)) :
ContMDiffOn I I' n f (โ‹ƒ (i : ฮน), s i) โ†” โˆ€ (i : ฮน), ContMDiffOn I I' n f (s i)

A function is C^k on a union of open sets s i iff it is C^k on each s i.

theorem contMDiff_of_contMDiffOn_iUnion_of_isOpen {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {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 โ„•โˆž} {ฮน : Type u_11} {s : ฮน โ†’ Set M} (hf : โˆ€ (i : ฮน), ContMDiffOn I I' n f (s i)) (hs : โˆ€ (i : ฮน), IsOpen (s i)) (hs' : โ‹ƒ (i : ฮน), s i = Set.univ) :
ContMDiff I I' n f

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 โ„•โˆž} {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
@[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 โ„•โˆž} {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

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 โ„•โˆž} {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 โ„•โˆž} {U : TopologicalSpace.Opens M} {f : โ†ฅU โ†’ 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 โ„•โˆž} {U : TopologicalSpace.Opens M} {f : โ†ฅU โ†’ 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 โ„•โˆž} {U V : TopologicalSpace.Opens M} (h : U โ‰ค V) :

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 โ„•โˆž} [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.

theorem contMDiffOn_isOpenEmbedding_symm {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ๐•œ E H} {M : Type u_4} [TopologicalSpace M] {e : M โ†’ H} (h : Topology.IsOpenEmbedding e) {n : WithTop โ„•โˆž} [Nonempty M] :

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 โ„•โˆž} [ChartedSpace H M] [Nonempty M'] {e' : M' โ†’ H'} (h' : Topology.IsOpenEmbedding e') {f : M โ†’ M'} (hf : ContMDiff I I' n (e' โˆ˜ f)) :
ContMDiff I I' n f

Let M' be a manifold whose chart structure is given by an open embedding e' into its model space H'. 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'.