Basic properties of smooth functions between manifolds

In this file, we show that standard operations on smooth maps between smooth manifolds are smooth:

• 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 smooth
• contMDiff_isOpenEmbedding shows that if M has a ChartedSpace structure induced by an open embedding e : M → H, then e is smooth.

Tags

chain rule, manifolds, higher derivative

Smoothness of the composition of smooth functions between manifolds

theorem ContMDiffWithinAt.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {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 : ℕ∞} {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 : ℕ∞} {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]

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

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 : ℕ∞} {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.

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

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 : ℕ∞} {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.

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

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 : ℕ∞} {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.

@[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 : ℕ∞} {g : M' → M''} (hg : ContMDiff I' I'' n g) (hf : ContMDiff I I' n f) : ContMDiff I I'' n (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 : ℕ∞} {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.

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

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 : ℕ∞} {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.

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

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 : ℕ∞} {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 : ℕ∞} {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]

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

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 : ℕ∞} {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

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

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 : ℕ∞} {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)

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

Alias of ContMDiffOn.comp_contMDiff.

The identity is smooth

theorem contMDiff_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : ℕ∞} : ContMDiff I I n id

@[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 : ℕ∞} : ContMDiff I I n id

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 : ℕ∞} : 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 : ℕ∞} : 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 : ℕ∞} : 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 : ℕ∞} : 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 : ℕ∞} : ContMDiffWithinAt I I n id s x

@[deprecated contMDiffWithinAt_id (since := "2024-11-20")]

theorem smoothWithinAt_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {n : ℕ∞} : ContMDiffWithinAt I I n id s x

Alias of contMDiffWithinAt_id.

Constants are smooth

theorem contMDiff_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [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 : ℕ∞} {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 : ℕ∞} [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 : ℕ∞} [Zero M'] : ContMDiffWithinAt I I' n 0 s x

Alias of contMDiffWithinAt_zero.

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 : ℕ∞} [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 : ℕ∞} [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_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 : ℕ∞) (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 : x ∉ tsupport f) (n : ℕ∞) (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 : x ∉ mulTSupport f) (n : ℕ∞) : 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 : x ∉ tsupport f) (n : ℕ∞) : ContMDiffAt I I' n f x

The inclusion map from one open set to another is smooth

theorem contMDiffAt_subtype_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {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 : ℕ∞} {U V : TopologicalSpace.Opens M} (h : U ≤ V) : ContMDiff I I n (TopologicalSpace.Opens.inclusion h)

@[deprecated contMDiffAt_subtype_iff (since := "2024-11-20")]

theorem smooth_subtype_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] {n : ℕ∞} {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.

@[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 : ℕ∞} {U : TopologicalSpace.Opens M} : ContMDiff I I n Subtype.val

Alias of contMDiff_subtype_val.

@[deprecated ContMDiff.extend_one (since := "2024-11-20")]

theorem Smooth.extend_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] [T2Space M] [One M'] {n : ℕ∞} {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)

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 : ℕ∞} {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)

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 : ℕ∞} {U V : TopologicalSpace.Opens M} (h : U ≤ V) : ContMDiff I I n (TopologicalSpace.Opens.inclusion h)

Alias of contMDiff_inclusion.

Open embeddings and their inverses are smooth

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

@[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 ℕ} [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 smooth.

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.toPartialHomeomorph 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 smooth.

@[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 ℕ} [Nonempty M] : ContMDiffOn I I n (↑(Topology.IsOpenEmbedding.toPartialHomeomorph e h).symm) (Set.range e)

Alias of contMDiffOn_isOpenEmbedding_symm.

---

If the ChartedSpace structure on a manifold M is given by an open embedding e : M → H, then the inverse of e is smooth.

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'. Then the smoothness of e' ∘ f : M → H' implies the smoothness of f.

This is useful, for example, when e' ∘ f = g ∘ e for smooth maps e : M → X and g : X → H'.

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

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'. Then the smoothness of e' ∘ f : M → H' implies the smoothness of f.

This is useful, for example, when e' ∘ f = g ∘ e for smooth maps e : M → X and g : X → H'.