# mathlib3documentation

geometry.manifold.cont_mdiff

# Smooth functions between smooth manifolds #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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'`.

• `cont_mdiff_within_at I I' n f s x` states that the function `f` is `Cⁿ` within the set `s` around the point `x`.
• `cont_mdiff_at I I' n f x` states that the function `f` is `Cⁿ` around `x`.
• `cont_mdiff_on I I' n f s` states that the function `f` is `Cⁿ` on the set `s`
• `cont_mdiff I I' n f` states that the function `f` is `Cⁿ`.
• `cont_mdiff_on.comp` gives the invariance of the `Cⁿ` property under composition
• `cont_mdiff_iff_cont_diff` 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 `cont_mdiff_within_at` and friends has to follow definitionally the setup of local invariant properties. Still, we recast the definition in terms of extended charts in `cont_mdiff_on_iff` and `cont_mdiff_iff`.

### Definition of smooth functions between manifolds #

def cont_diff_within_at_prop {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') (n : ℕ∞) (f : H H') (s : set H) (x : H) :
Prop

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
theorem cont_diff_within_at_prop_self_source {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {n : ℕ∞} {f : E H'} {s : set E} {x : E} :
f s x (I' f) s x
theorem cont_diff_within_at_prop_self {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_5} [ E'] {n : ℕ∞} {f : E E'} {s : set E} {x : E} :
f s x f s x
theorem cont_diff_within_at_prop_self_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {E' : Type u_5} [ E'] {n : ℕ∞} {f : H E'} {s : set H} {x : H} :
f s x (f (I.symm)) ((I.symm) ⁻¹' s (I x)
theorem cont_diff_within_at_local_invariant_prop {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') (n : ℕ∞) :
n)

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

theorem cont_diff_within_at_prop_mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') (n : ℕ∞) ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H H'⦄ (hts : s t) (h : n f s x) :
n f t x
theorem cont_diff_within_at_prop_id {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {n : ℕ∞} (x : H) :
x
def cont_mdiff_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (n : ℕ∞) (f : M M') (s : set M) (x : M) :
Prop

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
• n f s x = x
@[reducible]
def smooth_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (f : M M') (s : set M) (x : M) :
Prop

Abbreviation for `cont_mdiff_within_at I I' ⊤ f s x`. See also documentation for `smooth`.

Equations
• I' f s x = f s x
def cont_mdiff_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (n : ℕ∞) (f : M M') (x : M) :
Prop

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
theorem cont_mdiff_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] {n : ℕ∞} {f : M M'} {x : M} :
I' n f x ((ext_chart_at I' (f x)) f ((ext_chart_at I x).symm)) (set.range I) ( x) x)
@[reducible]
def smooth_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (f : M M') (x : M) :
Prop

Abbreviation for `cont_mdiff_at I I' ⊤ f x`. See also documentation for `smooth`.

Equations
• I' f x = I' f x
def cont_mdiff_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (n : ℕ∞) (f : M M') (s : set M) :
Prop

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
@[reducible]
def smooth_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (f : M M') (s : set M) :
Prop

Abbreviation for `cont_mdiff_on I I' ⊤ f s`. See also documentation for `smooth`.

Equations
• I' f s = I' f s
def cont_mdiff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (n : ℕ∞) (f : M M') :
Prop

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
• I' n f = (x : M), I' n f x
@[reducible]
def smooth {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} (I : H) {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} (I' : H') {M' : Type u_7} [ M'] (f : M M') :
Prop

Abbreviation for `cont_mdiff 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 `cont_diff`, it is still better to restate the lemma replacing `cont_diff` with `smooth` both in the assumption and in the conclusion, to make it possible to use `smooth` consistently. This also applies to `smooth_at`, `smooth_on` and `smooth_within_at`.

Equations

### Basic properties of smooth functions between manifolds #

theorem cont_mdiff.smooth {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} (h : I' f) :
I' f
theorem smooth.cont_mdiff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} (h : I' f) :
I' f
theorem cont_mdiff_on.smooth_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} (h : I' f s) :
I' f s
theorem smooth_on.cont_mdiff_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} (h : I' f s) :
I' f s
theorem cont_mdiff_at.smooth_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} (h : I' f x) :
I' f x
theorem smooth_at.cont_mdiff_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} (h : I' f x) :
I' f x
theorem cont_mdiff_within_at.smooth_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} (h : f s x) :
I' f s x
theorem smooth_within_at.cont_mdiff_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} (h : I' f s x) :
f s x
theorem cont_mdiff.cont_mdiff_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} {n : ℕ∞} (h : I' n f) :
I' n f x
theorem smooth.smooth_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} (h : I' f) :
I' f x
theorem cont_mdiff_within_at_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} {n : ℕ∞} :
n f set.univ x I' n f x
theorem smooth_within_at_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} :
I' f set.univ x I' f x
theorem cont_mdiff_on_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {n : ℕ∞} :
I' n f set.univ I' n f
theorem smooth_on_univ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} :
I' f set.univ I' f
theorem cont_mdiff_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} :
n f s x x ((ext_chart_at I' (f x)) f ((ext_chart_at I x).symm)) (((ext_chart_at I x).symm) ⁻¹' s ( x) 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 cont_mdiff_within_at_iff' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} :
n f s x x ((ext_chart_at I' (f x)) f ((ext_chart_at I x).symm)) ((ext_chart_at I x).target ((ext_chart_at I x).symm) ⁻¹' (s f ⁻¹' (ext_chart_at I' (f x)).source)) ( x) 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 `cont_mdiff_within_at_iff`, it is a smaller set, but their germs at `ext_chart_at I x x` are equal. It is sometimes useful to rewrite using this in the goal.

theorem cont_mdiff_within_at_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} :
n f s x x n ((ext_chart_at 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 smooth_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} :
I' f s x x ((ext_chart_at I' (f x)) f ((ext_chart_at I x).symm)) (((ext_chart_at I x).symm) ⁻¹' s ( x) x)
theorem smooth_within_at_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} :
I' f s x x ((ext_chart_at I' (f x)) f) s x
theorem cont_mdiff_at_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {n : ℕ∞} {x : M} :
I' n f x E') n ((ext_chart_at I' (f x)) f) x
theorem smooth_at_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} :
I' f x E') ((ext_chart_at I' (f x)) f) x
theorem cont_mdiff_within_at_iff_of_mem_maximal_atlas {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {e : H} {e' : H'} {f : M M'} {s : set M} {n : ℕ∞} {x : M} (he : e ) (he' : e' ) (hx : x e.to_local_equiv.source) (hy : f x e'.to_local_equiv.source) :
n f s x x ((e'.extend I') f ((e.extend I).symm)) (((e.extend I).symm) ⁻¹' s ((e.extend I) x)
theorem cont_mdiff_within_at_iff_image {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {e : H} {e' : H'} {f : M M'} {s : set M} {n : ℕ∞} {x : M} (he : e ) (he' : e' ) (hs : s e.to_local_equiv.source) (hx : x e.to_local_equiv.source) (hy : f x e'.to_local_equiv.source) :
n f s x x ((e'.extend I') f ((e.extend I).symm)) ((e.extend I) '' s) ((e.extend I) x)

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

theorem cont_mdiff_within_at_iff_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' ) (hy : f x' ) :
n f s x' x' ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) (((ext_chart_at I x).symm) ⁻¹' s ( x) 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 cont_mdiff_within_at_iff_of_mem_source' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' ) (hy : f x' ) :
n f s x' x' ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) ((ext_chart_at I x).target ((ext_chart_at I x).symm) ⁻¹' (s f ⁻¹' (ext_chart_at I' y).source)) ( x) x')
theorem cont_mdiff_at_iff_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' ) (hy : f x' ) :
I' n f x' x' ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) (set.range I) ( x) x')
theorem cont_mdiff_within_at_iff_target_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} {n : ℕ∞} {x : M} {y : M'} (hy : f x ) :
n f s x x n ((ext_chart_at I' y) f) s x
theorem cont_mdiff_at_iff_target_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {n : ℕ∞} {x : M} {y : M'} (hy : f x ) :
I' n f x E') n ((ext_chart_at I' y) f) x
theorem cont_mdiff_within_at_iff_source_of_mem_maximal_atlas {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {e : H} {f : M M'} {s : set M} {x : M} {n : ℕ∞} (he : e ) (hx : x e.to_local_equiv.source) :
n f s x n (f ((e.extend I).symm)) (((e.extend I).symm) ⁻¹' s ((e.extend I) x)
theorem cont_mdiff_within_at_iff_source_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} {x' : M} (hx' : x' ) :
n f s x' n (f ((ext_chart_at I x).symm)) (((ext_chart_at I x).symm) ⁻¹' s ( x) x')
theorem cont_mdiff_at_iff_source_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} {n : ℕ∞} {x' : M} (hx' : x' ) :
I' n f x' n (f ((ext_chart_at I x).symm)) (set.range I) ( x) x')
theorem cont_mdiff_on_iff_of_mem_maximal_atlas {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {e : H} {e' : H'} {f : M M'} {s : set M} {n : ℕ∞} (he : e ) (he' : e' ) (hs : s e.to_local_equiv.source) (h2s : s e'.to_local_equiv.source) :
I' n f s n ((e'.extend I') f ((e.extend I).symm)) ((e.extend I) '' s)
theorem cont_mdiff_on_iff_of_subset_source {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} {n : ℕ∞} {x : M} {y : M'} (hs : s ) (h2s : s ) :
I' n f s n ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) ( x) '' 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 `ext_chart_at I x '' s` instead of `(ext_chart_at I x).symm ⁻¹' s` to ensure that this set lies in `(ext_chart_at I x).target`.

theorem cont_mdiff_on_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} {n : ℕ∞} :
I' n f s (x : M) (y : M'), n ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) ((ext_chart_at I x).target ((ext_chart_at I x).symm) ⁻¹' (s f ⁻¹' (ext_chart_at I' y).source))

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

theorem cont_mdiff_on_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} {n : ℕ∞} :
I' n f s (y : M'), E') n ((ext_chart_at I' y) f) (s f ⁻¹' (ext_chart_at 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 smooth_on_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} :
I' f s (x : M) (y : M'), ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) ((ext_chart_at I x).target ((ext_chart_at I x).symm) ⁻¹' (s f ⁻¹' (ext_chart_at I' y).source))
theorem smooth_on_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} :
I' f s (y : M'), E') ((ext_chart_at I' y) f) (s f ⁻¹' (ext_chart_at I' y).source)
theorem cont_mdiff_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {n : ℕ∞} :
I' n f (x : M) (y : M'), n ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) ((ext_chart_at I x).target ((ext_chart_at I x).symm) ⁻¹' (f ⁻¹' (ext_chart_at I' y).source))

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

theorem cont_mdiff_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {n : ℕ∞} :
I' n f (y : M'), E') n ((ext_chart_at I' y) f) (f ⁻¹' (ext_chart_at 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} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} :
I' f (x : M) (y : M'), ((ext_chart_at I' y) f ((ext_chart_at I x).symm)) ((ext_chart_at I x).target ((ext_chart_at I x).symm) ⁻¹' (f ⁻¹' (ext_chart_at I' y).source))
theorem smooth_iff_target {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} :
I' f (y : M'), E') ((ext_chart_at I' y) f) (f ⁻¹' (ext_chart_at I' y).source)

### Deducing smoothness from higher smoothness #

theorem cont_mdiff_within_at.of_le {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {m n : ℕ∞} (hf : n f s x) (le : m n) :
m f s x
theorem cont_mdiff_at.of_le {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} {m n : ℕ∞} (hf : I' n f x) (le : m n) :
I' m f x
theorem cont_mdiff_on.of_le {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {m n : ℕ∞} (hf : I' n f s) (le : m n) :
I' m f s
theorem cont_mdiff.of_le {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {m n : ℕ∞} (hf : I' n f) (le : m n) :
I' m f

### Deducing smoothness from smoothness one step beyond #

theorem cont_mdiff_within_at.of_succ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : } (h : (n.succ) f s x) :
n f s x
theorem cont_mdiff_at.of_succ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} {n : } (h : I' (n.succ) f x) :
I' n f x
theorem cont_mdiff_on.of_succ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {n : } (h : I' (n.succ) f s) :
I' n f s
theorem cont_mdiff.of_succ {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {n : } (h : I' (n.succ) f) :
I' n f

### Deducing continuity from smoothness #

theorem cont_mdiff_within_at.continuous_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} (hf : n f s x) :
x
theorem cont_mdiff_at.continuous_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} {n : ℕ∞} (hf : I' n f x) :
theorem cont_mdiff_on.continuous_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {n : ℕ∞} (hf : I' n f s) :
theorem cont_mdiff.continuous {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {n : ℕ∞} (hf : I' n f) :

### `C^∞` smoothness #

theorem cont_mdiff_within_at_top {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} :
I' f s x (n : ), n f s x
theorem cont_mdiff_at_top {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {x : M} :
I' f x (n : ), I' n f x
theorem cont_mdiff_on_top {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} :
I' f s (n : ), I' n f s
theorem cont_mdiff_top {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} :
I' f (n : ), I' n f
theorem cont_mdiff_within_at_iff_nat {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} :
n f s x (m : ), m n m f s x

### Restriction to a smaller set #

theorem cont_mdiff_within_at.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s t : set M} {x : M} {n : ℕ∞} (hf : n f s x) (hts : s t) :
n f t x
theorem cont_mdiff_within_at.mono {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s t : set M} {x : M} {n : ℕ∞} (hf : n f s x) (hts : t s) :
n f t x
theorem cont_mdiff_within_at_congr_nhds {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s t : set M} {x : M} {n : ℕ∞} (hst : s = t) :
n f s x n f t x
theorem cont_mdiff_at.cont_mdiff_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} (hf : I' n f x) :
n f s x
theorem smooth_at.smooth_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} (hf : I' f x) :
I' f s x
theorem cont_mdiff_on.mono {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s t : set M} {n : ℕ∞} (hf : I' n f s) (hts : t s) :
I' n f t
theorem cont_mdiff.cont_mdiff_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {n : ℕ∞} (hf : I' n f) :
I' n f s
theorem smooth.smooth_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} (hf : I' f) :
I' f s
theorem cont_mdiff_within_at_inter' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s t : set M} {x : M} {n : ℕ∞} (ht : t s) :
n f (s t) x n f s x
theorem cont_mdiff_within_at_inter {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s t : set M} {x : M} {n : ℕ∞} (ht : t nhds x) :
n f (s t) x n f s x
theorem cont_mdiff_within_at.cont_mdiff_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} (h : n f s x) (ht : s nhds x) :
I' n f x
theorem smooth_within_at.smooth_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} (h : I' f s x) (ht : s nhds x) :
I' f x
theorem cont_mdiff_on.cont_mdiff_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} {n : ℕ∞} (h : I' n f s) (hx : s nhds x) :
I' n f x
theorem smooth_on.smooth_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {x : M} (h : I' f s) (hx : s nhds x) :
I' f x
theorem cont_mdiff_on_iff_source_of_mem_maximal_atlas {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {e : H} {f : M M'} {s : set M} {n : ℕ∞} (he : e ) (hs : s e.to_local_equiv.source) :
I' n f s I' n (f ((e.extend I).symm)) ((e.extend I) '' s)
theorem cont_mdiff_within_at_iff_cont_mdiff_on_nhds {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {s : set M} {x : M} {n : } :
n f s x (u : set M) (H_1 : u s)), 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 cont_mdiff_at_iff_cont_mdiff_on_nhds {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {x : M} {n : } :
I' n f x (u : set M) (H_1 : u nhds x), 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 cont_mdiff_at_iff_cont_mdiff_at_nhds {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] [I's : M'] {f : M M'} {x : M} {n : } :
I' n f x ∀ᶠ (x' : M) in nhds x, 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 cont_mdiff_within_at.congr {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {s : set M} {x : M} {n : ℕ∞} (h : n f s x) (h₁ : (y : M), y s f₁ y = f y) (hx : f₁ x = f x) :
n f₁ s x
theorem cont_mdiff_within_at_congr {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {s : set M} {x : M} {n : ℕ∞} (h₁ : (y : M), y s f₁ y = f y) (hx : f₁ x = f x) :
n f₁ s x n f s x
theorem cont_mdiff_within_at.congr_of_eventually_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {s : set M} {x : M} {n : ℕ∞} (h : n f s x) (h₁ : f₁ =ᶠ[ s] f) (hx : f₁ x = f x) :
n f₁ s x
theorem filter.eventually_eq.cont_mdiff_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {s : set M} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[ s] f) (hx : f₁ x = f x) :
n f₁ s x n f s x
theorem cont_mdiff_at.congr_of_eventually_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {x : M} {n : ℕ∞} (h : I' n f x) (h₁ : f₁ =ᶠ[nhds x] f) :
I' n f₁ x
theorem filter.eventually_eq.cont_mdiff_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[nhds x] f) :
I' n f₁ x I' n f x
theorem cont_mdiff_on.congr {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {s : set M} {n : ℕ∞} (h : I' n f s) (h₁ : (y : M), y s f₁ y = f y) :
I' n f₁ s
theorem cont_mdiff_on_congr {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f f₁ : M M'} {s : set M} {n : ℕ∞} (h₁ : (y : M), y s f₁ y = f y) :
I' n f₁ s I' n f s

### Locality #

theorem cont_mdiff_on_of_locally_cont_mdiff_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {s : set M} {n : ℕ∞} (h : (x : M), x s ( (u : set M), x u I' n f (s u))) :
I' n f s

Being `C^n` is a local property.

theorem cont_mdiff_of_locally_cont_mdiff_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {f : M M'} {n : ℕ∞} (h : (x : M), (u : set M), x u I' n f u) :
I' n f

### Smoothness of the composition of smooth functions between manifolds #

theorem cont_mdiff_within_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {n : ℕ∞} {t : set M'} {g : M' M''} (x : M) (hg : I'' n g t (f x)) (hf : n f s x) (st : s t) :
I'' n (g f) s x

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

theorem cont_mdiff_within_at.comp_of_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {n : ℕ∞} {t : set M'} {g : M' M''} {x : M} {y : M'} (hg : I'' n g t y) (hf : n f s x) (st : s t) (hx : f x = y) :
I'' n (g f) s x
theorem smooth_within_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {t : set M'} {g : M' M''} (x : M) (hg : I'' g t (f x)) (hf : I' f s x) (st : s t) :
I'' (g f) s x

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

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

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

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

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

theorem cont_mdiff_on.comp' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {n : ℕ∞} {t : set M'} {g : M' M''} (hg : I'' n g t) (hf : I' n f s) :
I'' n (g f) (s f ⁻¹' t)

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

theorem smooth_on.comp' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {t : set M'} {g : M' M''} (hg : I'' g t) (hf : I' f s) :
I'' (g f) (s f ⁻¹' t)

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

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

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

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

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

theorem cont_mdiff_within_at.comp' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {n : ℕ∞} {t : set M'} {g : M' M''} (x : M) (hg : I'' n g t (f x)) (hf : n f s x) :
I'' n (g f) (s f ⁻¹' t) x

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

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

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

theorem cont_mdiff_at.comp_cont_mdiff_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {n : ℕ∞} {g : M' M''} (x : M) (hg : I'' n g (f x)) (hf : n f s x) :
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 smooth_at.comp_smooth_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {s : set M} {g : M' M''} (x : M) (hg : I'' g (f x)) (hf : I' f s x) :
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 cont_mdiff_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {n : ℕ∞} {g : M' M''} (x : M) (hg : I'' n g (f x)) (hf : I' n f x) :
I'' n (g f) x

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

theorem cont_mdiff_at.comp_of_eq {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {n : ℕ∞} {g : M' M''} {x : M} {y : M'} (hg : I'' n g y) (hf : I' n f x) (hx : f x = y) :
I'' n (g f) x
theorem smooth_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {g : M' M''} (x : M) (hg : I'' g (f x)) (hf : I' f x) :
I'' (g f) x

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

theorem cont_mdiff.comp_cont_mdiff_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {n : ℕ∞} {f : M M'} {g : M' M''} {s : set M} (hg : I'' n g) (hf : I' n f s) :
I'' n (g f) s
theorem smooth.comp_smooth_on {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {g : M' M''} {s : set M} (hg : smooth I' I'' g) (hf : I' f s) :
I'' (g f) s
theorem cont_mdiff_on.comp_cont_mdiff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {n : ℕ∞} {t : set M'} {g : M' M''} (hg : I'' n g t) (hf : I' n f) (ht : (x : M), f x t) :
I'' n (g f)
theorem smooth_on.comp_smooth {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] {E' : Type u_5} [ E'] {H' : Type u_6} {I' : H'} {M' : Type u_7} [ M'] {E'' : Type u_8} [ E''] {H'' : Type u_9} [topological_space H''] {I'' : E'' H''} {M'' : Type u_10} [topological_space M''] [ M''] {f : M M'} {t : set M'} {g : M' M''} (hg : I'' g t) (hf : I' f) (ht : (x : M), f x t) :
I'' (g f)

### Atlas members are smooth #

theorem cont_mdiff_model {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {n : ℕ∞} :
n I
theorem cont_mdiff_on_model_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {n : ℕ∞} :
theorem cont_mdiff_on_of_mem_maximal_atlas {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {e : H} {n : ℕ∞} (h : e ) :

An atlas member is `C^n` for any `n`.

theorem cont_mdiff_on_symm_of_mem_maximal_atlas {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_3} {I : H} {M : Type u_4} [ M] [Is : M] {e : H} {n : ℕ∞} (h : e ) :

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

theorem cont_mdiff_at_of_mem_maximal_atlas {𝕜 : Type u_1} {E : Type u_2} [