Basic properties of C^n functions between manifolds

In this file, we show that standard operations on C^n maps between manifolds are C^n :

• ContMDiffOn.comp gives the invariance of the Cⁿ property under composition
• contMDiff_id gives the smoothness of the identity
• contMDiff_const gives the smoothness of constant functions
• contMDiff_inclusion shows that the inclusion between open sets of a topological space is C^n
• contMDiff_isOpenEmbedding shows that if M has a ChartedSpace structure induced by an open embedding e : M → H, then e is 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) : ContMDiffOn I I'' n (g ∘ f) (s ∩ f ⁻¹' t)

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) : ContMDiffWithinAt I I'' n (g ∘ f) (s ∩ f ⁻¹' t) 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 ℕ∞} : ContMDiff I I n 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 ℕ∞} : 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 ℕ∞} : ContMDiffWithinAt I I n id s x

Iterated functions

theorem ContMDiffOn.iterate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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 ℕ∞} {f : M → M} (hf : ContMDiffOn I I n f s) (hmaps : Set.MapsTo f s s) (k : ℕ) : ContMDiffOn I I n f^[k] s

The iterates of C^n functions on domains are C^n.

theorem ContMDiff.iterate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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 ℕ∞} {f : M → M} (hf : ContMDiff I I n f) (k : ℕ) : ContMDiff I I n f^[k]

The iterates of C^n functions are C^n.

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. See also contMDiff_section_of_tsupport for a similar result for sections of vector bundles.

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.

theorem ContMDiff.piecewise {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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 ℕ∞} {f g : M → M'} {s : Set M} [DecidablePred fun (x : M) => x ∈ s] (hf : ContMDiff I I' n f) (hg : ContMDiff I I' n g) (hfg : ∀ x ∈ frontier s, f =ᶠ[nhds x] g) : ContMDiff I I' n (s.piecewise f g)

Given two C^n functions f and g which coincide locally around the frontier of a set s, then the piecewise function defined using f on s and g elsewhere is C^n.

theorem ContMDiff.piecewise_Iic {n : WithTop ℕ∞} {E : Type u_11} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_12} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_13} [TopologicalSpace M] [ChartedSpace H M] {f g : ℝ → M} {s : ℝ} (hf : ContMDiff (modelWithCornersSelf ℝ ℝ) I n f) (hg : ContMDiff (modelWithCornersSelf ℝ ℝ) I n g) (hfg : f =ᶠ[nhds s] g) : ContMDiff (modelWithCornersSelf ℝ ℝ) I n ((Set.Iic s).piecewise f g)

Given two C^n functions f and g from ℝ to a real manifold which coincide locally around a point s, then the piecewise function using f before t and g after is C^n.

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

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} : ContMDiff I I n Subtype.val

theorem ContMDiff.extend_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] [T2Space M] [One M'] {n : WithTop ℕ∞} {U : TopologicalSpace.Opens M} {f : ↥U → M'} (supp : HasCompactMulSupport f) (diff : ContMDiff I I' n f) : ContMDiff I I' n (Function.extend Subtype.val f 1)

theorem ContMDiff.extend_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] [T2Space M] [Zero M'] {n : WithTop ℕ∞} {U : TopologicalSpace.Opens M} {f : ↥U → M'} (supp : HasCompactSupport f) (diff : ContMDiff I I' n f) : ContMDiff I I' n (Function.extend Subtype.val f 0)

theorem contMDiff_inclusion {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {U V : TopologicalSpace.Opens M} (h : U ≤ V) : ContMDiff I I n (TopologicalSpace.Opens.inclusion h)

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] : ContMDiffOn I I n (↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph e h).symm) (Set.range e)

If the ChartedSpace structure on a manifold M is given by an open embedding e : M → H, then the inverse of e is 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'.