# 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ⁿ.

We also give some basic properties of smooth functions between manifolds, following the API of smooth functions between vector spaces. See Basic.lean for further basic properties of smooth functions between smooth manifolds, NormedSpace.lean for the equivalence of manifold-smoothness to usual smoothness, Product.lean for smoothness results related to the product of manifolds and Atlas.lean for smoothness of atlas members and local structomorphisms.

## 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 LocalInvariantProperties.lean to get these properties automatically. For instance, the fact that being Cⁿ does not depend on the chart one considers is given by liftPropWithinAt_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.

Equations
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 I.symm) (I.symm ⁻¹' 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 : ℕ∞) :
().LocalInvariantProp () ()

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.

Equations
Instances For
@[reducible, inline]
abbrev 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.

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

Equations
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 ().symm) () (() x)
@[reducible, inline]
abbrev 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.

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

Equations
Instances For
@[reducible, inline]
abbrev 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.

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

Equations
Instances For
@[reducible, inline]
abbrev 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 ContMDiffFoo.bar will apply fine to an assumption SmoothFoo 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.

Equations
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 ().symm) (().symm ⁻¹' 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 ().symm) (().target ().symm ⁻¹' (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 ().symm) (().symm ⁻¹' 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' : } {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 ((e'.extend I') f (e.extend I).symm) ((e.extend I).symm ⁻¹' s ) ((e.extend I) 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' : } {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 ((e'.extend I') f (e.extend I).symm) ((e.extend I) '' s) ((e.extend I) 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).source) (hy : f x' (chartAt H' y).source) :
ContMDiffWithinAt I I' n f s x' ContDiffWithinAt 𝕜 n ((extChartAt I' y) f ().symm) (().symm ⁻¹' 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).source) (hy : f x' (chartAt H' y).source) :
ContMDiffWithinAt I I' n f s x' ContDiffWithinAt 𝕜 n ((extChartAt I' y) f ().symm) (().target ().symm ⁻¹' (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).source) (hy : f x' (chartAt H' y).source) :
ContMDiffAt I I' n f x' ContinuousAt f x' ContDiffWithinAt 𝕜 n ((extChartAt I' y) f ().symm) () (() 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).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).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 (e.extend I).symm) ((e.extend I).symm ⁻¹' s ) ((e.extend I) 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).source) :
ContMDiffWithinAt I I' n f s x' ContMDiffWithinAt () I' n (f ().symm) (().symm ⁻¹' 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).source) :
ContMDiffAt I I' n f x' ContMDiffWithinAt () I' n (f ().symm) () (() 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' : } {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 ((e'.extend I') f (e.extend I).symm) ((e.extend I) '' 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' : } {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 ((e'.extend I') f (e.extend I).symm) ((e.extend I) '' 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).source) (h2s : Set.MapsTo f s (chartAt H' y).source) :
ContMDiffOn I I' n f s ContDiffOn 𝕜 n ((extChartAt I' y) f ().symm) (() '' 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 ().symm) (() '' 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 ().symm) (().target ().symm ⁻¹' (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 ().symm) (().target ().symm ⁻¹' (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 ().symm) (().target ().symm ⁻¹' (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 ().symm) (().target ().symm ⁻¹' (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' (n.succ) 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' (n.succ) 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' (n.succ) 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' (n.succ) 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 (e.extend I).symm) ((e.extend I) '' 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 unhdsWithin 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 unhds 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₁ : ys, f₁ 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₁ : ys, f₁ 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₁ : ys, f₁ 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₁ : ys, f₁ y = f y) :
ContMDiffOn I I' n f₁ s ContMDiffOn I I' n f s
theorem ContMDiffOn.congr_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'} {f₁ : MM'} {s : Set M} {s₁ : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (h₁ : ys₁, f₁ y = f y) (hs : s₁ 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 : xs, ∃ (u : Set M), 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 : Set M), x u ContMDiffOn I I' n f u) :
ContMDiff I I' n f