Documentation

Mathlib.Geometry.Manifold.ContMDiff

Smooth functions between smooth manifolds #

We define Cⁿ functions between smooth manifolds, as functions which are Cⁿ in charts, and prove basic properties of these notions.

Main definitions and statements #

Let M  and M' be two smooth manifolds, with respect to model with corners I and I'. Let f : M → M'.

• ContMDiffWithinAt I I' n f s x states that the function f is Cⁿ within the set s around the point x.
• ContMDiffAt I I' n f x states that the function f is Cⁿ around x.
• ContMDiffOn I I' n f s states that the function f is Cⁿ on the set s
• ContMDiff I I' n f states that the function f is Cⁿ.
• ContMDiffOn.comp gives the invariance of the Cⁿ property under composition
• contMDiff_iff_contDiff states that, for functions between vector spaces, manifold-smoothness is equivalent to usual smoothness.

We also give many basic properties of smooth functions between manifolds, following the API of smooth functions between vector spaces.

Implementation details #

Many properties follow for free from the corresponding properties of functions in vector spaces, as being Cⁿ is a local property invariant under the smooth groupoid. We take advantage of the general machinery developed in local_invariant_properties.lean to get these properties automatically. For instance, the fact that being Cⁿ does not depend on the chart one considers is given by lift_prop_within_at_indep_chart.

For this to work, the definition of ContMDiffWithinAt and friends has to follow definitionally the setup of local invariant properties. Still, we recast the definition in terms of extended charts in contMDiffOn_iff and contMDiff_iff.

Definition of smooth functions between manifolds #

def ContDiffWithinAtProp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') (n : ℕ∞) (f : HH') (s : Set H) (x : H) :

Property in the model space of a model with corners of being C^n within at set at a point, when read in the model vector space. This property will be lifted to manifolds to define smooth functions between manifolds.

Instances For
theorem contDiffWithinAtProp_self_source {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {n : ℕ∞} {f : EH'} {s : Set E} {x : E} :
ContDiffWithinAtProp () I' n f s x ContDiffWithinAt 𝕜 n (I' f) s x
theorem contDiffWithinAtProp_self {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {n : ℕ∞} {f : EE'} {s : Set E} {x : E} :
ContDiffWithinAtProp () () n f s x ContDiffWithinAt 𝕜 n f s x
theorem contDiffWithinAtProp_self_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {E' : Type u_5} [] [NormedSpace 𝕜 E'] {n : ℕ∞} {f : HE'} {s : Set H} {x : H} :
ContDiffWithinAtProp I () n f s x ContDiffWithinAt 𝕜 n (f ) ( ⁻¹' s ) (I x)
theorem contDiffWithinAt_localInvariantProp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') (n : ℕ∞) :

Being Cⁿ in the model space is a local property, invariant under smooth maps. Therefore, it will lift nicely to manifolds.

theorem contDiffWithinAtProp_mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') (n : ℕ∞) ⦃s : Set H ⦃x : H ⦃t : Set H ⦃f : HH' (hts : s ) (h : ContDiffWithinAtProp I I' n f s x) :
theorem contDiffWithinAtProp_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {n : ℕ∞} (x : H) :
ContDiffWithinAtProp I I n id Set.univ x
def ContMDiffWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (s : Set M) (x : M) :

A function is n times continuously differentiable within a set at a point in a manifold if it is continuous and it is n times continuously differentiable in this set around this point, when read in the preferred chart at this point.

Instances For
@[reducible]
def SmoothWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (f : MM') (s : Set M) (x : M) :

Abbreviation for ContMDiffWithinAt I I' ⊤ f s x. See also documentation for Smooth.

Instances For
def ContMDiffAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (x : M) :

A function is n times continuously differentiable at a point in a manifold if it is continuous and it is n times continuously differentiable around this point, when read in the preferred chart at this point.

Instances For
theorem contMDiffAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] {n : ℕ∞} {f : MM'} {x : M} :
ContMDiffAt I I' n f x ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) f ↑()) () (↑() x)
@[reducible]
def SmoothAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (f : MM') (x : M) :

Abbreviation for ContMDiffAt I I' ⊤ f x. See also documentation for Smooth.

Instances For
def ContMDiffOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') (s : Set M) :

A function is n times continuously differentiable in a set of a manifold if it is continuous and, for any pair of points, it is n times continuously differentiable on this set in the charts around these points.

Instances For
@[reducible]
def SmoothOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (f : MM') (s : Set M) :

Abbreviation for ContMDiffOn I I' ⊤ f s. See also documentation for Smooth.

Instances For
def ContMDiff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (n : ℕ∞) (f : MM') :

A function is n times continuously differentiable in a manifold if it is continuous and, for any pair of points, it is n times continuously differentiable in the charts around these points.

Instances For
@[reducible]
def Smooth {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] (f : MM') :

Abbreviation for ContMDiff I I' ⊤ f. Short note to work with these abbreviations: a lemma of the form cont_mdiff_foo.bar will apply fine to an assumption smooth_foo using dot notation or normal notation. If the consequence bar of the lemma involves ContDiff, it is still better to restate the lemma replacing ContDiff with Smooth both in the assumption and in the conclusion, to make it possible to use Smooth consistently. This also applies to SmoothAt, SmoothOn and SmoothWithinAt.

Instances For

Deducing smoothness from higher smoothness #

theorem ContMDiffWithinAt.of_le {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {m : ℕ∞} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (le : m n) :
ContMDiffWithinAt I I' m f s x
theorem ContMDiffAt.of_le {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {m : ℕ∞} {n : ℕ∞} (hf : ContMDiffAt I I' n f x) (le : m n) :
ContMDiffAt I I' m f x
theorem ContMDiffOn.of_le {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {m : ℕ∞} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (le : m n) :
ContMDiffOn I I' m f s
theorem ContMDiff.of_le {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {m : ℕ∞} {n : ℕ∞} (hf : ContMDiff I I' n f) (le : m n) :
ContMDiff I I' m f

Basic properties of smooth functions between manifolds #

theorem ContMDiff.smooth {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} (h : ContMDiff I I' f) :
Smooth I I' f
theorem Smooth.contMDiff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} (h : Smooth I I' f) :
ContMDiff I I' n f
theorem ContMDiffOn.smoothOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} (h : ContMDiffOn I I' f s) :
SmoothOn I I' f s
theorem SmoothOn.contMDiffOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (h : SmoothOn I I' f s) :
ContMDiffOn I I' n f s
theorem ContMDiffAt.smoothAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} (h : ContMDiffAt I I' f x) :
SmoothAt I I' f x
theorem SmoothAt.contMDiffAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} (h : SmoothAt I I' f x) :
ContMDiffAt I I' n f x
theorem ContMDiffWithinAt.smoothWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} (h : ContMDiffWithinAt I I' f s x) :
SmoothWithinAt I I' f s x
theorem SmoothWithinAt.contMDiffWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : SmoothWithinAt I I' f s x) :
ContMDiffWithinAt I I' n f s x
theorem ContMDiff.contMDiffAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} (h : ContMDiff I I' n f) :
ContMDiffAt I I' n f x
theorem Smooth.smoothAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} (h : Smooth I I' f) :
SmoothAt I I' f x
theorem contMDiffWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I' n f Set.univ x ContMDiffAt I I' n f x
theorem smoothWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} :
SmoothWithinAt I I' f Set.univ x SmoothAt I I' f x
theorem contMDiffOn_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} :
ContMDiffOn I I' n f Set.univ ContMDiff I I' n f
theorem smoothOn_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} :
SmoothOn I I' f Set.univ Smooth I I' f
theorem contMDiffWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I' n f s x ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) f ↑()) (↑() ⁻¹' s ) (↑() x)

One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart.

theorem contMDiffWithinAt_iff' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I' n f s x ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) f ↑()) (().target ↑() ⁻¹' (s f ⁻¹' (extChartAt I' (f x)).source)) (↑() x)

One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart. This form states smoothness of f written in such a way that the set is restricted to lie within the domain/codomain of the corresponding charts. Even though this expression is more complicated than the one in contMDiffWithinAt_iff, it is a smaller set, but their germs at extChartAt I x x are equal. It is sometimes useful to rewrite using this in the goal.

theorem contMDiffWithinAt_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I' n f s x ContMDiffWithinAt I () n (↑(extChartAt I' (f x)) f) s x

One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart in the target.

theorem smoothWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} :
SmoothWithinAt I I' f s x ContDiffWithinAt 𝕜 (↑(extChartAt I' (f x)) f ↑()) (↑() ⁻¹' s ) (↑() x)
theorem smoothWithinAt_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} :
SmoothWithinAt I I' f s x SmoothWithinAt I () (↑(extChartAt I' (f x)) f) s x
theorem contMDiffAt_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} {x : M} :
ContMDiffAt I I' n f x ContMDiffAt I () n (↑(extChartAt I' (f x)) f) x
theorem smoothAt_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} :
SmoothAt I I' f x SmoothAt I () (↑(extChartAt I' (f x)) f) x
theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {e : } {e' : LocalHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} {x : M} (he : ) (he' : ) (hx : x e.source) (hy : f x e'.source) :
ContMDiffWithinAt I I' n f s x ContDiffWithinAt 𝕜 n (↑() f ↑()) (↑() ⁻¹' s ) (↑() x)
theorem contMDiffWithinAt_iff_image {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {e : } {e' : LocalHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} {x : M} (he : ) (he' : ) (hs : s e.source) (hx : x e.source) (hy : f x e'.source) :
ContMDiffWithinAt I I' n f s x ContDiffWithinAt 𝕜 n (↑() f ↑()) (↑() '' s) (↑() x)

An alternative formulation of contMDiffWithinAt_iff_of_mem_maximalAtlas if the set if s lies in e.source.

theorem contMDiffWithinAt_iff_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' (chartAt H x).toLocalEquiv.source) (hy : f x' (chartAt H' y).toLocalEquiv.source) :
ContMDiffWithinAt I I' n f s x' ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) f ↑()) (↑() ⁻¹' s ) (↑() x')

One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in any chart containing that point.

theorem contMDiffWithinAt_iff_of_mem_source' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' (chartAt H x).toLocalEquiv.source) (hy : f x' (chartAt H' y).toLocalEquiv.source) :
ContMDiffWithinAt I I' n f s x' ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) f ↑()) (().target ↑() ⁻¹' (s f ⁻¹' (extChartAt I' y).source)) (↑() x')
theorem contMDiffAt_iff_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' (chartAt H x).toLocalEquiv.source) (hy : f x' (chartAt H' y).toLocalEquiv.source) :
ContMDiffAt I I' n f x' ContinuousAt f x' ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) f ↑()) () (↑() x')
theorem contMDiffWithinAt_iff_target_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {n : ℕ∞} {x : M} {y : M'} (hy : f x (chartAt H' y).toLocalEquiv.source) :
ContMDiffWithinAt I I' n f s x ContMDiffWithinAt I () n (↑(extChartAt I' y) f) s x
theorem contMDiffAt_iff_target_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {n : ℕ∞} {x : M} {y : M'} (hy : f x (chartAt H' y).toLocalEquiv.source) :
ContMDiffAt I I' n f x ContMDiffAt I () n (↑(extChartAt I' y) f) x
theorem contMDiffWithinAt_iff_source_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {e : } {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (he : ) (hx : x e.source) :
ContMDiffWithinAt I I' n f s x ContMDiffWithinAt () I' n (f ↑()) (↑() ⁻¹' s ) (↑() x)
theorem contMDiffWithinAt_iff_source_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} {x' : M} (hx' : x' (chartAt H x).toLocalEquiv.source) :
ContMDiffWithinAt I I' n f s x' ContMDiffWithinAt () I' n (f ↑()) (↑() ⁻¹' s ) (↑() x')
theorem contMDiffAt_iff_source_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} {x' : M} (hx' : x' (chartAt H x).toLocalEquiv.source) :
ContMDiffAt I I' n f x' ContMDiffWithinAt () I' n (f ↑()) () (↑() x')
theorem contMDiffOn_iff_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {e : } {e' : LocalHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} (he : ) (he' : ) (hs : s e.source) (h2s : Set.MapsTo f s e'.source) :
ContMDiffOn I I' n f s ContDiffOn 𝕜 n (↑() f ↑()) (↑() '' s)
theorem contMDiffOn_iff_of_mem_maximalAtlas' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {e : } {e' : LocalHomeomorph M' H'} {f : MM'} {s : Set M} {n : ℕ∞} (he : ) (he' : ) (hs : s e.source) (h2s : Set.MapsTo f s e'.source) :
ContMDiffOn I I' n f s ContDiffOn 𝕜 n (↑() f ↑()) (↑() '' s)
theorem contMDiffOn_iff_of_subset_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {n : ℕ∞} {x : M} {y : M'} (hs : s (chartAt H x).toLocalEquiv.source) (h2s : Set.MapsTo f s (chartAt H' y).toLocalEquiv.source) :
ContMDiffOn I I' n f s ContDiffOn 𝕜 n (↑(extChartAt I' y) f ↑()) (↑() '' s)

If the set where you want f to be smooth lies entirely in a single chart, and f maps it into a single chart, the smoothness of f on that set can be expressed by purely looking in these charts. Note: this lemma uses extChartAt I x '' s instead of (extChartAt I x).symm ⁻¹' s to ensure that this set lies in (extChartAt I x).target.

theorem contMDiffOn_iff_of_subset_source' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {n : ℕ∞} {x : M} {y : M'} (hs : s ().source) (h2s : Set.MapsTo f s (extChartAt I' y).source) :
ContMDiffOn I I' n f s ContDiffOn 𝕜 n (↑(extChartAt I' y) f ↑()) (↑() '' s)

If the set where you want f to be smooth lies entirely in a single chart, and f maps it into a single chart, the smoothness of f on that set can be expressed by purely looking in these charts. Note: this lemma uses extChartAt I x '' s instead of (extChartAt I x).symm ⁻¹' s to ensure that this set lies in (extChartAt I x).target.

theorem contMDiffOn_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {n : ℕ∞} :
ContMDiffOn I I' n f s ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) f ↑()) (().target ↑() ⁻¹' (s f ⁻¹' (extChartAt I' y).source))

One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.

theorem contMDiffOn_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {n : ℕ∞} :
ContMDiffOn I I' n f s ∀ (y : M'), ContMDiffOn I () n (↑(extChartAt I' y) f) (s f ⁻¹' (extChartAt I' y).source)

One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.

theorem smoothOn_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} :
SmoothOn I I' f s ∀ (x : M) (y : M'), ContDiffOn 𝕜 (↑(extChartAt I' y) f ↑()) (().target ↑() ⁻¹' (s f ⁻¹' (extChartAt I' y).source))
theorem smoothOn_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} :
SmoothOn I I' f s ∀ (y : M'), SmoothOn I () (↑(extChartAt I' y) f) (s f ⁻¹' (extChartAt I' y).source)
theorem contMDiff_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {n : ℕ∞} :
ContMDiff I I' n f ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) f ↑()) (().target ↑() ⁻¹' (f ⁻¹' (extChartAt I' y).source))

One can reformulate smoothness as continuity and smoothness in any extended chart.

theorem contMDiff_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {n : ℕ∞} :
ContMDiff I I' n f ∀ (y : M'), ContMDiffOn I () n (↑(extChartAt I' y) f) (f ⁻¹' (extChartAt I' y).source)

One can reformulate smoothness as continuity and smoothness in any extended chart in the target.

theorem smooth_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} :
Smooth I I' f ∀ (x : M) (y : M'), ContDiffOn 𝕜 (↑(extChartAt I' y) f ↑()) (().target ↑() ⁻¹' (f ⁻¹' (extChartAt I' y).source))
theorem smooth_iff_target {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} :
Smooth I I' f ∀ (y : M'), SmoothOn I () (↑(extChartAt I' y) f) (f ⁻¹' (extChartAt I' y).source)

Deducing smoothness from smoothness one step beyond #

theorem ContMDiffWithinAt.of_succ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : } (h : ContMDiffWithinAt I I' (↑()) f s x) :
ContMDiffWithinAt I I' (n) f s x
theorem ContMDiffAt.of_succ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {n : } (h : ContMDiffAt I I' (↑()) f x) :
ContMDiffAt I I' (n) f x
theorem ContMDiffOn.of_succ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : } (h : ContMDiffOn I I' (↑()) f s) :
ContMDiffOn I I' (n) f s
theorem ContMDiff.of_succ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {n : } (h : ContMDiff I I' (↑()) f) :
ContMDiff I I' (n) f

Deducing continuity from smoothness #

theorem ContMDiffWithinAt.continuousWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) :
theorem ContMDiffAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} (hf : ContMDiffAt I I' n f x) :
theorem ContMDiffOn.continuousOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) :
theorem ContMDiff.continuous {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} (hf : ContMDiff I I' n f) :

C^∞ smoothness #

theorem contMDiffWithinAt_top {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} :
SmoothWithinAt I I' f s x ∀ (n : ), ContMDiffWithinAt I I' (n) f s x
theorem contMDiffAt_top {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} :
SmoothAt I I' f x ∀ (n : ), ContMDiffAt I I' (n) f x
theorem contMDiffOn_top {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} :
SmoothOn I I' f s ∀ (n : ), ContMDiffOn I I' (n) f s
theorem contMDiff_top {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} :
Smooth I I' f ∀ (n : ), ContMDiff I I' (n) f
theorem contMDiffWithinAt_iff_nat {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I' n f s x ∀ (m : ), m nContMDiffWithinAt I I' (m) f s x

Restriction to a smaller set #

theorem ContMDiffWithinAt.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (hts : s ) :
ContMDiffWithinAt I I' n f t x
theorem ContMDiffWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (hts : t s) :
ContMDiffWithinAt I I' n f t x
theorem contMDiffWithinAt_congr_nhds {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} {x : M} {n : ℕ∞} (hst : = ) :
ContMDiffWithinAt I I' n f s x ContMDiffWithinAt I I' n f t x
theorem contMDiffWithinAt_insert_self {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I' n f (insert x s) x ContMDiffWithinAt I I' n f s x
theorem ContMDiffWithinAt.of_insert {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I' n f (insert x s) xContMDiffWithinAt I I' n f s x

Alias of the forward direction of contMDiffWithinAt_insert_self.

theorem ContMDiffWithinAt.insert {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) :
ContMDiffWithinAt I I' n f (insert x s) x
theorem ContMDiffAt.contMDiffWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (hf : ContMDiffAt I I' n f x) :
ContMDiffWithinAt I I' n f s x
theorem SmoothAt.smoothWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} (hf : SmoothAt I I' f x) :
SmoothWithinAt I I' f s x
theorem ContMDiffOn.mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (hts : t s) :
ContMDiffOn I I' n f t
theorem ContMDiff.contMDiffOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (hf : ContMDiff I I' n f) :
ContMDiffOn I I' n f s
theorem Smooth.smoothOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} (hf : Smooth I I' f) :
SmoothOn I I' f s
theorem contMDiffWithinAt_inter' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} {x : M} {n : ℕ∞} (ht : t ) :
ContMDiffWithinAt I I' n f (s t) x ContMDiffWithinAt I I' n f s x
theorem contMDiffWithinAt_inter {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} {x : M} {n : ℕ∞} (ht : t nhds x) :
ContMDiffWithinAt I I' n f (s t) x ContMDiffWithinAt I I' n f s x
theorem ContMDiffWithinAt.contMDiffAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (ht : s nhds x) :
ContMDiffAt I I' n f x
theorem SmoothWithinAt.smoothAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} (h : SmoothWithinAt I I' f s x) (ht : s nhds x) :
SmoothAt I I' f x
theorem ContMDiffOn.contMDiffAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffOn I I' n f s) (hx : s nhds x) :
ContMDiffAt I I' n f x
theorem SmoothOn.smoothAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} (h : SmoothOn I I' f s) (hx : s nhds x) :
SmoothAt I I' f x
theorem contMDiffOn_iff_source_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {e : } {f : MM'} {s : Set M} {n : ℕ∞} (he : ) (hs : s e.source) :
ContMDiffOn I I' n f s ContMDiffOn () I' n (f ↑()) (↑() '' s)
theorem contMDiffWithinAt_iff_contMDiffOn_nhds {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {s : Set M} {x : M} {n : } :
ContMDiffWithinAt I I' (n) f s x u, u nhdsWithin x (insert x s) ContMDiffOn I I' (n) f u

A function is C^n within a set at a point, for n : ℕ, if and only if it is C^n on a neighborhood of this point.

theorem contMDiffAt_iff_contMDiffOn_nhds {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {x : M} {n : } :
ContMDiffAt I I' (n) f x u, u nhds x ContMDiffOn I I' (n) f u

A function is C^n at a point, for n : ℕ, if and only if it is C^n on a neighborhood of this point.

theorem contMDiffAt_iff_contMDiffAt_nhds {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] [] {f : MM'} {x : M} {n : } :
ContMDiffAt I I' (n) f x ∀ᶠ (x' : M) in nhds x, ContMDiffAt I I' (n) f x'

Note: This does not hold for n = ∞. f being C^∞ at x means that for every n, f is C^n on some neighborhood of x, but this neighborhood can depend on n.

Congruence lemmas #

theorem ContMDiffWithinAt.congr {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (h₁ : ∀ (y : M), y sf₁ y = f y) (hx : f₁ x = f x) :
ContMDiffWithinAt I I' n f₁ s x
theorem contMDiffWithinAt_congr {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h₁ : ∀ (y : M), y sf₁ y = f y) (hx : f₁ x = f x) :
ContMDiffWithinAt I I' n f₁ s x ContMDiffWithinAt I I' n f s x
theorem ContMDiffWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h : ContMDiffWithinAt I I' n f s x) (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
ContMDiffWithinAt I I' n f₁ s x
theorem Filter.EventuallyEq.contMDiffWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
ContMDiffWithinAt I I' n f₁ s x ContMDiffWithinAt I I' n f s x
theorem ContMDiffAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {n : ℕ∞} (h : ContMDiffAt I I' n f x) (h₁ : f₁ =ᶠ[nhds x] f) :
ContMDiffAt I I' n f₁ x
theorem Filter.EventuallyEq.contMDiffAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[nhds x] f) :
ContMDiffAt I I' n f₁ x ContMDiffAt I I' n f x
theorem ContMDiffOn.congr {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} {n : ℕ∞} (h : ContMDiffOn I I' n f s) (h₁ : ∀ (y : M), y sf₁ y = f y) :
ContMDiffOn I I' n f₁ s
theorem contMDiffOn_congr {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} {n : ℕ∞} (h₁ : ∀ (y : M), y sf₁ y = f y) :
ContMDiffOn I I' n f₁ s ContMDiffOn I I' n f s

Locality #

theorem contMDiffOn_of_locally_contMDiffOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (h : ∀ (x : M), x su, x u ContMDiffOn I I' n f (s u)) :
ContMDiffOn I I' n f s

Being C^n is a local property.

theorem contMDiff_of_locally_contMDiffOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} (h : ∀ (x : M), u, x u ContMDiffOn I I' n f u) :
ContMDiff I I' n f

Smoothness of the composition of smooth functions between manifolds #

theorem ContMDiffWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {n : ℕ∞} {t : Set M'} {g : M'M''} {x : M} {y : M'} (hg : ContMDiffWithinAt I' I'' n g t y) (hf : ContMDiffWithinAt I I' n f s x) (st : Set.MapsTo f s t) (hx : f x = y) :
ContMDiffWithinAt I I'' n (g f) s x

See note [comp_of_eq lemmas]

theorem SmoothWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {t : Set M'} {g : M'M''} (x : M) (hg : SmoothWithinAt I' I'' g t (f x)) (hf : SmoothWithinAt I I' f s x) (st : Set.MapsTo f s t) :
SmoothWithinAt I I'' (g f) s x

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

theorem ContMDiffOn.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {n : ℕ∞} {t : Set M'} {g : M'M''} (hg : ContMDiffOn I' I'' n g t) (hf : ContMDiffOn I I' n f s) (st : s f ⁻¹' t) :
ContMDiffOn I I'' n (g f) s

The composition of C^n functions on domains is C^n.

theorem SmoothOn.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {t : Set M'} {g : M'M''} (hg : SmoothOn I' I'' g t) (hf : SmoothOn I I' f s) (st : s f ⁻¹' t) :
SmoothOn I I'' (g f) s

The composition of C^∞ functions on domains is C^∞.

theorem ContMDiffOn.comp' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {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.

theorem SmoothOn.comp' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {t : Set M'} {g : M'M''} (hg : SmoothOn I' I'' g t) (hf : SmoothOn I I' f s) :
SmoothOn I I'' (g f) (s f ⁻¹' t)

The composition of C^∞ functions is C^∞.

theorem ContMDiff.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {n : ℕ∞} {g : M'M''} (hg : ContMDiff I' I'' n g) (hf : ContMDiff I I' n f) :
ContMDiff I I'' n (g f)

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

theorem Smooth.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : M'M''} (hg : Smooth I' I'' g) (hf : Smooth I I' f) :
Smooth I I'' (g f)

The composition of C^∞ functions is C^∞.

theorem ContMDiffWithinAt.comp' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {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.

theorem SmoothWithinAt.comp' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {t : Set M'} {g : M'M''} (x : M) (hg : SmoothWithinAt I' I'' g t (f x)) (hf : SmoothWithinAt I I' f s x) :
SmoothWithinAt I I'' (g f) (s f ⁻¹' t) x

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

theorem ContMDiffAt.comp_contMDiffWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {n : ℕ∞} {g : M'M''} (x : M) (hg : ContMDiffAt I' I'' n g (f x)) (hf : ContMDiffWithinAt I I' n f s x) :
ContMDiffWithinAt I I'' n (g f) s x

g ∘ f is C^n within s at x if g is C^n at f x and f is C^n within s at x.

theorem SmoothAt.comp_smoothWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {g : M'M''} (x : M) (hg : SmoothAt I' I'' g (f x)) (hf : SmoothWithinAt I I' f s x) :
SmoothWithinAt I I'' (g f) s x

g ∘ f is C^∞ within s at x if g is C^∞ at f x and f is C^∞ within s at x.

theorem ContMDiffAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {n : ℕ∞} {g : M'M''} {x : M} {y : M'} (hg : ContMDiffAt I' I'' n g y) (hf : ContMDiffAt I I' n f x) (hx : f x = y) :
ContMDiffAt I I'' n (g f) x

See note [comp_of_eq lemmas]

theorem SmoothAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : M'M''} (x : M) (hg : SmoothAt I' I'' g (f x)) (hf : SmoothAt I I' f x) :
SmoothAt I I'' (g f) x

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

theorem ContMDiff.comp_contMDiffOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {n : ℕ∞} {f : MM'} {g : M'M''} {s : Set M} (hg : ContMDiff I' I'' n g) (hf : ContMDiffOn I I' n f s) :
ContMDiffOn I I'' n (g f) s
theorem Smooth.comp_smoothOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : M'M''} {s : Set M} (hg : Smooth I' I'' g) (hf : SmoothOn I I' f s) :
SmoothOn I I'' (g f) s
theorem ContMDiffOn.comp_contMDiff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {n : ℕ∞} {t : Set M'} {g : M'M''} (hg : ContMDiffOn I' I'' n g t) (hf : ContMDiff I I' n f) (ht : ∀ (x : M), f x t) :
ContMDiff I I'' n (g f)
theorem SmoothOn.comp_smooth {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {t : Set M'} {g : M'M''} (hg : SmoothOn I' I'' g t) (hf : Smooth I I' f) (ht : ∀ (x : M), f x t) :
Smooth I I'' (g f)

Atlas members are smooth #

theorem contMDiff_model {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {n : ℕ∞} :
ContMDiff I () n I
theorem contMDiffOn_model_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {n : ℕ∞} :
ContMDiffOn () I n () ()
theorem contMDiffOn_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} (h : ) :
ContMDiffOn I I n (e) e.source

An atlas member is C^n for any n.

theorem contMDiffOn_symm_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} (h : ) :
ContMDiffOn I I n (↑()) e.target

The inverse of an atlas member is C^n for any n.

theorem contMDiffAt_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {x : M} {n : ℕ∞} (h : ) (hx : x e.source) :
ContMDiffAt I I n (e) x
theorem contMDiffAt_symm_of_mem_maximalAtlas {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} {x : H} (h : ) (hx : x e.target) :
ContMDiffAt I I n (↑()) x
theorem contMDiffOn_chart {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffOn I I n (↑(chartAt H x)) (chartAt H x).toLocalEquiv.source
theorem contMDiffOn_chart_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffOn I I n (↑()) (chartAt H x).toLocalEquiv.target
theorem contMDiffAt_extend {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} {x : M} (he : ) (hx : x e.source) :
ContMDiffAt I () n (↑()) x
theorem contMDiffAt_extChartAt' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} {x' : M} (h : x' (chartAt H x).toLocalEquiv.source) :
ContMDiffAt I () n (↑()) x'
theorem contMDiffAt_extChartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffAt I () n (↑()) x
theorem contMDiffOn_extChartAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffOn I () n (↑()) (chartAt H x).toLocalEquiv.source
theorem contMDiffOn_extend_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {e : } {n : ℕ∞} (he : ) :
ContMDiffOn () I n (↑()) (I '' e.target)
theorem contMDiffOn_extChartAt_symm {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {n : ℕ∞} (x : M) :
ContMDiffOn () I n (↑()) ().target
theorem contMDiffOn_of_mem_contDiffGroupoid {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {n : ℕ∞} {e' : } (h : e' ) :
ContMDiffOn I I n (e') e'.source

An element of contDiffGroupoid ⊤ I is C^n for any n.

The identity is smooth #

theorem contMDiff_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {n : ℕ∞} :
ContMDiff I I n id
theorem smooth_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] :
Smooth I I id
theorem contMDiffOn_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {n : ℕ∞} :
ContMDiffOn I I n id s
theorem smoothOn_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} :
SmoothOn I I id s
theorem contMDiffAt_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {n : ℕ∞} :
ContMDiffAt I I n id x
theorem smoothAt_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} :
SmoothAt I I id x
theorem contMDiffWithinAt_id {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {x : M} {n : ℕ∞} :
ContMDiffWithinAt I I n id s x