mathlib documentation

geometry.manifold.cont_mdiff

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

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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {n : ℕ∞} {f : E → H'} {s : set E} {x : E} :
theorem cont_diff_within_at_prop_self {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {s : set E} {x : E} :
theorem cont_diff_within_at_prop_self_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : H → E'} {s : set H} {x : H} :
theorem cont_diff_within_at_local_invariant_prop {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 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 cont_diff_within_at_prop_mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') (n : ℕ∞) ⦃s : set H⦄ ⦃x : H⦄ ⦃t : set H⦄ ⦃f : H → H'⦄ (hts : t s) (h : cont_diff_within_at_prop I I' n f s x) :
theorem cont_diff_within_at_prop_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) (x : H) :
def cont_mdiff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' 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
@[reducible]
def smooth_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' 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
def cont_mdiff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : ℕ∞} {f : M → M'} {x : M} :
@[reducible]
def smooth_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M → M') (x : M) :
Prop

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

Equations
def cont_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M → M') (s : set M) :
Prop

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

Equations
def cont_mdiff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' 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
@[reducible]
def smooth {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} (h : cont_mdiff I I' f) :
smooth I I' f
theorem smooth.cont_mdiff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} (h : smooth I I' f) :
theorem cont_mdiff_on.smooth_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} (h : cont_mdiff_on I I' f s) :
smooth_on I I' f s
theorem smooth_on.cont_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} (h : smooth_on I I' f s) :
theorem cont_mdiff_at.smooth_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} (h : cont_mdiff_at I I' f x) :
smooth_at I I' f x
theorem smooth_at.cont_mdiff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} (h : smooth_at I I' f x) :
theorem cont_mdiff_within_at.smooth_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} (h : cont_mdiff_within_at I I' f s x) :
smooth_within_at I I' f s x
theorem smooth_within_at.cont_mdiff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} (h : smooth_within_at I I' f s x) :
theorem cont_mdiff.cont_mdiff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} {n : ℕ∞} (h : cont_mdiff I I' n f) :
cont_mdiff_at I I' n f x
theorem smooth.smooth_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} (h : smooth I I' f) :
smooth_at I I' f x
theorem cont_mdiff_within_at_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} {n : ℕ∞} :
theorem smooth_within_at_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} :
theorem cont_mdiff_on_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {n : ℕ∞} :
theorem smooth_on_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} :
theorem cont_mdiff_within_at_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} :

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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} :

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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} :

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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} :
theorem smooth_within_at_iff_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} :
theorem cont_mdiff_at_iff_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {n : ℕ∞} {x : M} :
theorem smooth_at_iff_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} :
theorem cont_mdiff_within_at_iff_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' (charted_space.chart_at H x).to_local_equiv.source) (hy : f x' (charted_space.chart_at H' y).to_local_equiv.source) :

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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' (charted_space.chart_at H x).to_local_equiv.source) (hy : f x' (charted_space.chart_at H' y).to_local_equiv.source) :
theorem cont_mdiff_at_iff_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {x : M} {n : ℕ∞} {x' : M} {y : M'} (hx : x' (charted_space.chart_at H x).to_local_equiv.source) (hy : f x' (charted_space.chart_at H' y).to_local_equiv.source) :
theorem cont_mdiff_within_at_iff_target_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {n : ℕ∞} {x : M} {y : M'} (hy : f x (charted_space.chart_at H' y).to_local_equiv.source) :
theorem cont_mdiff_at_iff_target_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {n : ℕ∞} {x : M} {y : M'} (hy : f x (charted_space.chart_at H' y).to_local_equiv.source) :
theorem model_with_corners.symm_continuous_within_at_comp_right_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {X : Type u_4} [topological_space X] {f : H → X} {s : set H} {x : H} :
theorem ext_chart_at_symm_continuous_within_at_comp_right_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {X : Type u_5} [topological_space X] {f : M → X} {s : set M} {x x' : M} :
theorem cont_mdiff_within_at_iff_source_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} {x' : M} (hx' : x' (charted_space.chart_at H x).to_local_equiv.source) :
theorem cont_mdiff_at_iff_source_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} {n : ℕ∞} {x' : M} (hx' : x' (charted_space.chart_at H x).to_local_equiv.source) :
theorem cont_mdiff_at_ext_chart_at' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {x : M} {n : ℕ∞} {x' : M} (h : x' (charted_space.chart_at H x).to_local_equiv.source) :
theorem cont_mdiff_at_ext_chart_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {x : M} {n : ℕ∞} :
theorem cont_mdiff_on_iff_of_subset_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {n : ℕ∞} {x : M} {y : M'} (hs : s (charted_space.chart_at H x).to_local_equiv.source) (h2s : set.maps_to f s (charted_space.chart_at H' y).to_local_equiv.source) :

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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {n : ℕ∞} :
cont_mdiff_on I I' n f s continuous_on f s ∀ (x : M) (y : M'), cont_diff_on 𝕜 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {n : ℕ∞} :
cont_mdiff_on I I' n f s continuous_on f s ∀ (y : M'), cont_mdiff_on I (model_with_corners_self 𝕜 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} :
smooth_on I I' f s continuous_on f s ∀ (x : M) (y : M'), cont_diff_on 𝕜 ((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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} :
smooth_on I I' f s continuous_on f s ∀ (y : M'), smooth_on I (model_with_corners_self 𝕜 E') ((ext_chart_at I' y) f) (s f ⁻¹' (ext_chart_at I' y).source)
theorem cont_mdiff_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {n : ℕ∞} :
cont_mdiff I I' n f continuous f ∀ (x : M) (y : M'), cont_diff_on 𝕜 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {n : ℕ∞} :
cont_mdiff I I' n f continuous f ∀ (y : M'), cont_mdiff_on I (model_with_corners_self 𝕜 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} :
smooth I I' f continuous f ∀ (x : M) (y : M'), cont_diff_on 𝕜 ((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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} :
smooth I I' f continuous f ∀ (y : M'), smooth_on I (model_with_corners_self 𝕜 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} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {m n : ℕ∞} (hf : cont_mdiff_within_at I I' n f s x) (le : m n) :
theorem cont_mdiff_at.of_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} {m n : ℕ∞} (hf : cont_mdiff_at I I' n f x) (le : m n) :
cont_mdiff_at I I' m f x
theorem cont_mdiff_on.of_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {m n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (le : m n) :
cont_mdiff_on I I' m f s
theorem cont_mdiff.of_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {m n : ℕ∞} (hf : cont_mdiff I I' n f) (le : m n) :
cont_mdiff I I' m f

Deducing smoothness from smoothness one step beyond #

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

Deducing continuity from smoothness #

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

Deducing differentiability from smoothness #

theorem cont_mdiff_within_at.mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} (hf : cont_mdiff_within_at I I' n f s x) (hn : 1 n) :
theorem cont_mdiff_at.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} {n : ℕ∞} (hf : cont_mdiff_at I I' n f x) (hn : 1 n) :
theorem cont_mdiff_on.mdifferentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (hn : 1 n) :
theorem cont_mdiff.mdifferentiable {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {n : ℕ∞} (hf : cont_mdiff I I' n f) (hn : 1 n) :
theorem smooth.mdifferentiable {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} (hf : smooth I I' f) :
theorem smooth.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} (hf : smooth I I' f) :
theorem smooth.mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} (hf : smooth I I' f) :

C^∞ smoothness #

theorem cont_mdiff_within_at_top {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} :
smooth_within_at I I' f s x ∀ (n : ), cont_mdiff_within_at I I' n f s x
theorem cont_mdiff_at_top {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {x : M} :
smooth_at I I' f x ∀ (n : ), cont_mdiff_at I I' n f x
theorem cont_mdiff_on_top {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} :
smooth_on I I' f s ∀ (n : ), cont_mdiff_on I I' n f s
theorem cont_mdiff_top {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} :
smooth I I' f ∀ (n : ), cont_mdiff I I' n f
theorem cont_mdiff_within_at_iff_nat {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} :
cont_mdiff_within_at I I' n f s x ∀ (m : ), m ncont_mdiff_within_at I I' m f s x

Restriction to a smaller set #

theorem cont_mdiff_within_at.mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s t : set M} {x : M} {n : ℕ∞} (hf : cont_mdiff_within_at I I' n f s x) (hts : t s) :
theorem cont_mdiff_at.cont_mdiff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} (hf : cont_mdiff_at I I' n f x) :
theorem smooth_at.smooth_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} (hf : smooth_at I I' f x) :
smooth_within_at I I' f s x
theorem cont_mdiff_on.mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s t : set M} {n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (hts : t s) :
cont_mdiff_on I I' n f t
theorem cont_mdiff.cont_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} (hf : cont_mdiff I I' n f) :
cont_mdiff_on I I' n f s
theorem smooth.smooth_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} (hf : smooth I I' f) :
smooth_on I I' f s
theorem cont_mdiff_within_at_inter' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s t : set M} {x : M} {n : ℕ∞} (ht : t nhds_within x s) :
cont_mdiff_within_at I I' n f (s t) x cont_mdiff_within_at I I' n f s x
theorem cont_mdiff_within_at_inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s t : set M} {x : M} {n : ℕ∞} (ht : t nhds x) :
cont_mdiff_within_at I I' n f (s t) x cont_mdiff_within_at I I' n f s x
theorem cont_mdiff_within_at.cont_mdiff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} (h : cont_mdiff_within_at I I' n f s x) (ht : s nhds x) :
cont_mdiff_at I I' n f x
theorem smooth_within_at.smooth_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} (h : smooth_within_at I I' f s x) (ht : s nhds x) :
smooth_at I I' f x
theorem cont_mdiff_on.cont_mdiff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} (h : cont_mdiff_on I I' n f s) (hx : s nhds x) :
cont_mdiff_at I I' n f x
theorem smooth_on.smooth_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {x : M} (h : smooth_on I I' f s) (hx : s nhds x) :
smooth_at I I' f x
theorem cont_mdiff_on_ext_chart_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {x : M} {n : ℕ∞} :
theorem cont_mdiff_within_at_iff_cont_mdiff_on_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {x : M} {n : } :
cont_mdiff_within_at I I' n f s x ∃ (u : set M) (H_1 : u nhds_within x (has_insert.insert x s)), cont_mdiff_on 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 cont_mdiff_at_iff_cont_mdiff_on_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {x : M} {n : } :
cont_mdiff_at I I' n f x ∃ (u : set M) (H_1 : u nhds x), cont_mdiff_on 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 cont_mdiff_at_iff_cont_mdiff_at_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {x : M} {n : } :
cont_mdiff_at I I' n f x ∀ᶠ (x' : M) in nhds x, cont_mdiff_at 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 cont_mdiff_within_at.congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {s : set M} {x : M} {n : ℕ∞} (h : cont_mdiff_within_at I I' n f s x) (h₁ : ∀ (y : M), y sf₁ y = f y) (hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x
theorem cont_mdiff_within_at_congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {s : set M} {x : M} {n : ℕ∞} (h₁ : ∀ (y : M), y sf₁ y = f y) (hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x cont_mdiff_within_at I I' n f s x
theorem cont_mdiff_within_at.congr_of_eventually_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {s : set M} {x : M} {n : ℕ∞} (h : cont_mdiff_within_at I I' n f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x
theorem filter.eventually_eq.cont_mdiff_within_at_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {s : set M} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x cont_mdiff_within_at I I' n f s x
theorem cont_mdiff_at.congr_of_eventually_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {x : M} {n : ℕ∞} (h : cont_mdiff_at I I' n f x) (h₁ : f₁ =ᶠ[nhds x] f) :
cont_mdiff_at I I' n f₁ x
theorem filter.eventually_eq.cont_mdiff_at_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {x : M} {n : ℕ∞} (h₁ : f₁ =ᶠ[nhds x] f) :
cont_mdiff_at I I' n f₁ x cont_mdiff_at I I' n f x
theorem cont_mdiff_on.congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {s : set M} {n : ℕ∞} (h : cont_mdiff_on I I' n f s) (h₁ : ∀ (y : M), y sf₁ y = f y) :
cont_mdiff_on I I' n f₁ s
theorem cont_mdiff_on_congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M → M'} {s : set M} {n : ℕ∞} (h₁ : ∀ (y : M), y sf₁ y = f y) :
cont_mdiff_on I I' n f₁ s cont_mdiff_on I I' n f s

Locality #

theorem cont_mdiff_on_of_locally_cont_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} (h : ∀ (x : M), x s(∃ (u : set M), is_open u x u cont_mdiff_on I I' n f (s u))) :
cont_mdiff_on I I' n f s

Being C^n is a local property.

theorem cont_mdiff_of_locally_cont_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {n : ℕ∞} (h : ∀ (x : M), ∃ (u : set M), is_open u x u cont_mdiff_on I I' n f u) :
cont_mdiff I I' n f

Smoothness of the composition of smooth functions between manifolds #

theorem cont_mdiff_within_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {t : set M'} {g : M' → M''} (x : M) (hg : cont_mdiff_within_at I' I'' n g t (f x)) (hf : cont_mdiff_within_at I I' n f s x) (st : set.maps_to f s t) :
cont_mdiff_within_at I I'' n (g f) s x

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

theorem cont_mdiff_on.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {t : set M'} {g : M' → M''} (hg : cont_mdiff_on I' I'' n g t) (hf : cont_mdiff_on I I' n f s) (st : s f ⁻¹' t) :
cont_mdiff_on I I'' n (g f) s

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

theorem cont_mdiff_on.comp' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {t : set M'} {g : M' → M''} (hg : cont_mdiff_on I' I'' n g t) (hf : cont_mdiff_on I I' n f s) :
cont_mdiff_on I I'' n (g f) (s f ⁻¹' t)

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

theorem cont_mdiff.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {g : M' → M''} (hg : cont_mdiff I' I'' n g) (hf : cont_mdiff I I' n f) :
cont_mdiff I I'' n (g f)

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

theorem cont_mdiff_within_at.comp' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {t : set M'} {g : M' → M''} (x : M) (hg : cont_mdiff_within_at I' I'' n g t (f x)) (hf : cont_mdiff_within_at I I' n f s x) :
cont_mdiff_within_at I I'' n (g f) (s f ⁻¹' t) x

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

theorem cont_mdiff_at.comp_cont_mdiff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {s : set M} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {g : M' → M''} (x : M) (hg : cont_mdiff_at I' I'' n g (f x)) (hf : cont_mdiff_within_at I I' n f s x) :
cont_mdiff_within_at 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 cont_mdiff_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {g : M' → M''} (x : M) (hg : cont_mdiff_at I' I'' n g (f x)) (hf : cont_mdiff_at I I' n f x) :
cont_mdiff_at I I'' n (g f) x

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

theorem cont_mdiff.comp_cont_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {f : M → M'} {g : M' → M''} {s : set M} (hg : cont_mdiff I' I'' n g) (hf : cont_mdiff_on I I' n f s) :
cont_mdiff_on I I'' n (g f) s
theorem smooth.comp_smooth_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {f : M → M'} {g : M' → M''} {s : set M} (hg : smooth I' I'' g) (hf : smooth_on I I' f s) :
smooth_on I I'' (g f) s
theorem cont_mdiff_on.comp_cont_mdiff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {n : ℕ∞} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {t : set M'} {g : M' → M''} (hg : cont_mdiff_on I' I'' n g t) (hf : cont_mdiff I I' n f) (ht : ∀ (x : M), f x t) :
cont_mdiff I I'' n (g f)
theorem smooth_on.comp_smooth {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M → M'} {E'' : Type u_14} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_15} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_16} [topological_space M''] [charted_space H'' M''] {t : set M'} {g : M' → M''} (hg : smooth_on I' I'' g t) (hf : smooth I I' f) (ht : ∀ (x : M), f x t) :
smooth I I'' (g f)

Atlas members are smooth #

An atlas member is C^n for any n.

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

theorem cont_mdiff_on_chart {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {x : M} {n : ℕ∞} :
theorem cont_mdiff_on_chart_symm {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {x : M} {n : ℕ∞} :

The identity is smooth #

theorem cont_mdiff_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {n : ℕ∞} :
theorem smooth_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] :
theorem cont_mdiff_on_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {n : ℕ∞} :
theorem smooth_on_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} :
theorem cont_mdiff_at_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {n : ℕ∞} :
theorem smooth_at_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} :
theorem cont_mdiff_within_at_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {x : M} {n : ℕ∞} :
theorem smooth_within_at_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {x : M} :

Constants are smooth #

theorem cont_mdiff_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : ℕ∞} {c : M'} :
cont_mdiff I I' n (λ (x : M), c)
theorem cont_mdiff_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : ℕ∞} [has_zero M'] :
cont_mdiff I I' n 0
theorem cont_mdiff_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {n : ℕ∞} [has_one M'] :
cont_mdiff I I' n 1
theorem smooth_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {c : M'} :
smooth I I' (λ (x : M), c)
theorem smooth_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [has_one M'] :
smooth I I' 1
theorem smooth_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [has_zero M'] :
smooth I I' 0
theorem cont_mdiff_on_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {n : ℕ∞} {c : M'} :
cont_mdiff_on I I' n (λ (x : M), c) s
theorem cont_mdiff_on_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {n : ℕ∞} [has_zero M'] :
cont_mdiff_on I I' n 0 s
theorem cont_mdiff_on_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {n : ℕ∞} [has_one M'] :
cont_mdiff_on I I' n 1 s
theorem smooth_on_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {c : M'} :
smooth_on I I' (λ (x : M), c) s
theorem smooth_on_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} [has_one M'] :
smooth_on I I' 1 s
theorem smooth_on_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} [has_zero M'] :
smooth_on I I' 0 s
theorem cont_mdiff_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {x : M} {n : ℕ∞} {c : M'} :
cont_mdiff_at I I' n (λ (x : M), c) x
theorem cont_mdiff_at_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {x : M} {n : ℕ∞} [has_zero M'] :
cont_mdiff_at I I' n 0 x
theorem cont_mdiff_at_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {x : M} {n : ℕ∞} [has_one M'] :
cont_mdiff_at I I' n 1 x
theorem smooth_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {x : M} {c : M'} :
smooth_at I I' (λ (x : M), c) x
theorem smooth_at_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {x : M} [has_zero M'] :
smooth_at I I' 0 x
theorem smooth_at_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {x : M} [has_one M'] :
smooth_at I I' 1 x
theorem cont_mdiff_within_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {x : M} {n : ℕ∞} {c : M'} :
cont_mdiff_within_at I I' n (λ (x : M), c) s x
theorem cont_mdiff_within_at_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {x : M} {n : ℕ∞} [has_one M'] :
theorem cont_mdiff_within_at_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {x : M} {n : ℕ∞} [has_zero M'] :
theorem smooth_within_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {x : M} {c : M'} :
smooth_within_at I I' (λ (x : M), c) s x
theorem smooth_within_at_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {x : M} [has_zero M'] :
smooth_within_at I I' 0 s x
theorem smooth_within_at_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} {x : M} [has_one M'] :
smooth_within_at I I' 1 s x
theorem cont_mdiff_of_support {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f : M → F} (hf : ∀ (x : M), x tsupport fcont_mdiff_at I (model_with_corners_self 𝕜 F) n f x) :

Equivalence with the basic definition for functions between vector spaces #

theorem cont_mdiff_within_at_iff_cont_diff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {s : set E} {x : E} :
theorem cont_mdiff_within_at.cont_diff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {s : set E} {x : E} :

Alias of the forward direction of cont_mdiff_within_at_iff_cont_diff_within_at.

theorem cont_diff_within_at.cont_mdiff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {s : set E} {x : E} :

Alias of the reverse direction of cont_mdiff_within_at_iff_cont_diff_within_at.

theorem cont_mdiff_at_iff_cont_diff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {x : E} :
theorem cont_diff_at.cont_mdiff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {x : E} :

Alias of the reverse direction of cont_mdiff_at_iff_cont_diff_at.

theorem cont_mdiff_at.cont_diff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {x : E} :

Alias of the forward direction of cont_mdiff_at_iff_cont_diff_at.

theorem cont_mdiff_on_iff_cont_diff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {s : set E} :
theorem cont_mdiff_on.cont_diff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {s : set E} :

Alias of the forward direction of cont_mdiff_on_iff_cont_diff_on.

theorem cont_diff_on.cont_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} {s : set E} :

Alias of the reverse direction of cont_mdiff_on_iff_cont_diff_on.

theorem cont_mdiff_iff_cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} :
theorem cont_diff.cont_mdiff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} :

Alias of the reverse direction of cont_mdiff_iff_cont_diff.

theorem cont_mdiff.cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {n : ℕ∞} {f : E → E'} :

Alias of the forward direction of cont_mdiff_iff_cont_diff.

The tangent map of a smooth function is smooth #

theorem cont_mdiff_on.continuous_on_tangent_map_within_aux {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {n : ℕ∞} {f : H → H'} {s : set H} (hf : cont_mdiff_on I I' n f s) (hn : 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n with 1 ≤ n on a domain with unique derivatives, then its bundled derivative is continuous. In this auxiliary lemma, we prove this fact when the source and target space are model spaces in models with corners. The general fact is proved in cont_mdiff_on.continuous_on_tangent_map_within

theorem cont_mdiff_on.cont_mdiff_on_tangent_map_within_aux {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {m n : ℕ∞} {f : H → H'} {s : set H} (hf : cont_mdiff_on I I' n f s) (hmn : m + 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n on a domain with unique derivatives, then its bundled derivative is C^m when m+1 ≤ n. In this auxiliary lemma, we prove this fact when the source and target space are model spaces in models with corners. The general fact is proved in cont_mdiff_on.cont_mdiff_on_tangent_map_within

theorem cont_mdiff_on.cont_mdiff_on_tangent_map_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {m n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (hmn : m + 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n on a domain with unique derivatives, then its bundled derivative is C^m when m+1 ≤ n.

theorem cont_mdiff_on.continuous_on_tangent_map_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {s : set M} {n : ℕ∞} (hf : cont_mdiff_on I I' n f s) (hmn : 1 n) (hs : unique_mdiff_on I s) :

If a function is C^n on a domain with unique derivatives, with 1 ≤ n, then its bundled derivative is continuous there.

theorem cont_mdiff.cont_mdiff_tangent_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {m n : ℕ∞} (hf : cont_mdiff I I' n f) (hmn : m + 1 n) :

If a function is C^n, then its bundled derivative is C^m when m+1 ≤ n.

theorem cont_mdiff.continuous_tangent_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M'] {f : M → M'} {n : ℕ∞} (hf : cont_mdiff I I' n f) (hmn : 1 n) :

If a function is C^n, with 1 ≤ n, then its bundled derivative is continuous.

Smoothness of the projection in a basic smooth bundle #

theorem basic_smooth_vector_bundle_core.cont_mdiff_at_iff_target {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] (Z : basic_smooth_vector_bundle_core I M E') {f : N → Z.to_topological_vector_bundle_core.total_space} {x : N} {n : ℕ∞} :

A version of cont_mdiff_at_iff_target when the codomain is the total space of a basic_smooth_vector_bundle_core. The continuity condition in the RHS is weaker.

theorem basic_smooth_vector_bundle_core.smooth_const_section {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (Z : basic_smooth_vector_bundle_core I M E') (v : E') (h : ∀ (i j : (charted_space.atlas H M)) (x : M), x i.val.to_local_equiv.source j.val.to_local_equiv.source(Z.coord_change i j ((i.val) x)) v = v) :
smooth I (I.prod (model_with_corners_self 𝕜 E')) (show M → Z.to_topological_vector_bundle_core.total_space, from λ (x : M), x, v⟩)

If an element of E' is invariant under all coordinate changes, then one can define a corresponding section of the fiber bundle, which is smooth. This applies in particular to the zero section of a vector bundle. Another example (not yet defined) would be the identity section of the endomorphism bundle of a vector bundle.

Smoothness of the tangent bundle projection #

theorem tangent_bundle.cont_mdiff_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {n : ℕ∞} :
theorem tangent_bundle.smooth_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] :
theorem tangent_bundle.cont_mdiff_on_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {n : ℕ∞} {s : set (tangent_bundle I M)} :
theorem tangent_bundle.smooth_on_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {s : set (tangent_bundle I M)} :
theorem tangent_bundle.cont_mdiff_at_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {n : ℕ∞} {p : tangent_bundle I M} :
theorem tangent_bundle.smooth_at_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {p : tangent_bundle I M} :
theorem tangent_bundle.cont_mdiff_within_at_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {n : ℕ∞} {s : set (tangent_bundle I M)} {p : tangent_bundle I M} :
theorem tangent_bundle.smooth_within_at_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] {s : set (tangent_bundle I M)} {p : tangent_bundle I M} :
def tangent_bundle.zero_section {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) (M : Type u_4) [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] :
M → tangent_bundle I M

The zero section of the tangent bundle

Equations
theorem tangent_bundle.smooth_zero_section {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] :
theorem tangent_bundle.tangent_map_tangent_bundle_pure {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [Is : smooth_manifold_with_corners I M] (p : tangent_bundle I M) :

The derivative of the zero section of the tangent bundle maps ⟨x, v⟩ to ⟨⟨x, 0⟩, ⟨v, 0⟩⟩.

Note that, as currently framed, this is a statement in coordinates, thus reliant on the choice of the coordinate system we use on the tangent bundle.

However, the result itself is coordinate-dependent only to the extent that the coordinates determine a splitting of the tangent bundle. Moreover, there is a canonical splitting at each point of the zero section (since there is a canonical horizontal space there, the tangent space to the zero section, in addition to the canonical vertical space which is the kernel of the derivative of the projection), and this canonical splitting is also the one that comes from the coordinates on the tangent bundle in our definitions. So this statement is not as crazy as it may seem.

TODO define splittings of vector bundles; state this result invariantly.

Smoothness of standard maps associated to the product of manifolds #

theorem cont_mdiff_within_at.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {s : set M} {x : M} {n : ℕ∞} {f : M → M'} {g : M → N'} (hf : cont_mdiff_within_at I I' n f s x) (hg : cont_mdiff_within_at I J' n g s x) :
cont_mdiff_within_at I (I'.prod J') n (λ (x : M), (f x, g x)) s x
theorem cont_mdiff_within_at.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {s : set M} {x : M} {n : ℕ∞} {f : M → E'} {g : M → F'} (hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 E') n f s x) (hg : cont_mdiff_within_at I (model_with_corners_self 𝕜 F') n g s x) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x)) s x
theorem cont_mdiff_at.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {x : M} {n : ℕ∞} {f : M → M'} {g : M → N'} (hf : cont_mdiff_at I I' n f x) (hg : cont_mdiff_at I J' n g x) :
cont_mdiff_at I (I'.prod J') n (λ (x : M), (f x, g x)) x
theorem cont_mdiff_at.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {x : M} {n : ℕ∞} {f : M → E'} {g : M → F'} (hf : cont_mdiff_at I (model_with_corners_self 𝕜 E') n f x) (hg : cont_mdiff_at I (model_with_corners_self 𝕜 F') n g x) :
cont_mdiff_at I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x)) x
theorem cont_mdiff_on.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {s : set M} {n : ℕ∞} {f : M → M'} {g : M → N'} (hf : cont_mdiff_on I I' n f s) (hg : cont_mdiff_on I J' n g s) :
cont_mdiff_on I (I'.prod J') n (λ (x : M), (f x, g x)) s
theorem cont_mdiff_on.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {s : set M} {n : ℕ∞} {f : M → E'} {g : M → F'} (hf : cont_mdiff_on I (model_with_corners_self 𝕜 E') n f s) (hg : cont_mdiff_on I (model_with_corners_self 𝕜 F') n g s) :
cont_mdiff_on I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x)) s
theorem cont_mdiff.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {n : ℕ∞} {f : M → M'} {g : M → N'} (hf : cont_mdiff I I' n f) (hg : cont_mdiff I J' n g) :
cont_mdiff I (I'.prod J') n (λ (x : M), (f x, g x))
theorem cont_mdiff.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {n : ℕ∞} {f : M → E'} {g : M → F'} (hf : cont_mdiff I (model_with_corners_self 𝕜 E') n f) (hg : cont_mdiff I (model_with_corners_self 𝕜 F') n g) :
cont_mdiff I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x))
theorem smooth_within_at.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {s : set M} {x : M} {f : M → M'} {g : M → N'} (hf : smooth_within_at I I' f s x) (hg : smooth_within_at I J' g s x) :
smooth_within_at I (I'.prod J') (λ (x : M), (f x, g x)) s x
theorem smooth_within_at.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {s : set M} {x : M} {f : M → E'} {g : M → F'} (hf : smooth_within_at I (model_with_corners_self 𝕜 E') f s x) (hg : smooth_within_at I (model_with_corners_self 𝕜 F') g s x) :
smooth_within_at I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x)) s x
theorem smooth_at.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {x : M} {f : M → M'} {g : M → N'} (hf : smooth_at I I' f x) (hg : smooth_at I J' g x) :
smooth_at I (I'.prod J') (λ (x : M), (f x, g x)) x
theorem smooth_at.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {x : M} {f : M → E'} {g : M → F'} (hf : smooth_at I (model_with_corners_self 𝕜 E') f x) (hg : smooth_at I (model_with_corners_self 𝕜 F') g x) :
smooth_at I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x)) x
theorem smooth_on.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {s : set M} {f : M → M'} {g : M → N'} (hf : smooth_on I I' f s) (hg : smooth_on I J' g s) :
smooth_on I (I'.prod J') (λ (x : M), (f x, g x)) s
theorem smooth_on.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {s : set M} {f : M → E'} {g : M → F'} (hf : smooth_on I (model_with_corners_self 𝕜 E') f s) (hg : smooth_on I (model_with_corners_self 𝕜 F') g s) :
smooth_on I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x)) s
theorem smooth.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {g : M → N'} (hf : smooth I I' f) (hg : smooth I J' g) :
smooth I (I'.prod J') (λ (x : M), (f x, g x))
theorem smooth.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {f : M → E'} {g : M → F'} (hf : smooth I (model_with_corners_self 𝕜 E') f) (hg : smooth I (model_with_corners_self 𝕜 F') g) :
smooth I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x))
theorem cont_mdiff_within_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} {s : set (M × N)} {p : M × N} :
theorem cont_mdiff_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} {p : M × N} :
theorem cont_mdiff_on_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} {s : set (M × N)} :
theorem cont_mdiff_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} :
theorem smooth_within_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {s : set (M × N)} {p : M × N} :
theorem smooth_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {p : M × N} :
theorem smooth_on_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {s : set (M × N)} :
theorem smooth_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] :
theorem cont_mdiff_within_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} {s : set (M × N)} {p : M × N} :
theorem cont_mdiff_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} {p : M × N} :
theorem cont_mdiff_on_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} {s : set (M × N)} :
theorem cont_mdiff_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {n : ℕ∞} :
theorem smooth_within_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {s : set (M × N)} {p : M × N} :
theorem smooth_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {p : M × N} :
theorem smooth_on_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {s : set (M × N)} :
theorem smooth_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] :
theorem smooth_iff_proj_smooth {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M' × N'} :
smooth I (I'.prod J') f smooth I I' (prod.fst f) smooth I J' (prod.snd f)
theorem cont_mdiff_within_at.prod_map' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {s : set M} {n : ℕ∞} {g : N → N'} {r : set N} {p : M × N} (hf : cont_mdiff_within_at I I' n f s p.fst) (hg : cont_mdiff_within_at J J' n g r p.snd) :
cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s ×ˢ r) p

The product map of two C^n functions within a set at a point is C^n within the product set at the product point.

theorem cont_mdiff_within_at.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {s : set M} {x : M} {n : ℕ∞} {g : N → N'} {r : set N} {y : N} (hf : cont_mdiff_within_at I I' n f s x) (hg : cont_mdiff_within_at J J' n g r y) :
cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s ×ˢ r) (x, y)
theorem cont_mdiff_at.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {x : M} {n : ℕ∞} {g : N → N'} {y : N} (hf : cont_mdiff_at I I' n f x) (hg : cont_mdiff_at J J' n g y) :
cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) (x, y)
theorem cont_mdiff_at.prod_map' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {n : ℕ∞} {g : N → N'} {p : M × N} (hf : cont_mdiff_at I I' n f p.fst) (hg : cont_mdiff_at J J' n g p.snd) :
cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) p
theorem cont_mdiff_on.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {s : set M} {n : ℕ∞} {g : N → N'} {r : set N} (hf : cont_mdiff_on I I' n f s) (hg : cont_mdiff_on J J' n g r) :
cont_mdiff_on (I.prod J) (I'.prod J') n (prod.map f g) (s ×ˢ r)
theorem cont_mdiff.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {n : ℕ∞} {g : N → N'} (hf : cont_mdiff I I' n f) (hg : cont_mdiff J J' n g) :
cont_mdiff (I.prod J) (I'.prod J') n (prod.map f g)
theorem smooth_within_at.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {s : set M} {x : M} {g : N → N'} {r : set N} {y : N} (hf : smooth_within_at I I' f s x) (hg : smooth_within_at J J' g r y) :
smooth_within_at (I.prod J) (I'.prod J') (prod.map f g) (s ×ˢ r) (x, y)
theorem smooth_at.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {x : M} {g : N → N'} {y : N} (hf : smooth_at I I' f x) (hg : smooth_at J J' g y) :
smooth_at (I.prod J) (I'.prod J') (prod.map f g) (x, y)
theorem smooth_on.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {s : set M} {g : N → N'} {r : set N} (hf : smooth_on I I' f s) (hg : smooth_on J J' g r) :
smooth_on (I.prod J) (I'.prod J') (prod.map f g) (s ×ˢ r)
theorem smooth.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_9} [topological_space G] {J : model_with_corners 𝕜 F G} {N : Type u_10} [topological_space N] [charted_space G N] {F' : Type u_11} [normed_add_comm_group F'] [normed_space 𝕜 F'] {G' : Type u_12} [topological_space G'] {J' : model_with_corners 𝕜 F' G'} {N' : Type u_13} [topological_space N'] [charted_space G' N'] {f : M → M'} {g : N → N'} (hf : smooth I I' f) (hg : smooth J J' g) :
smooth (I.prod J) (I'.prod J') (prod.map f g)

Smoothness of functions with codomain Π i, F i #

We have no model_with_corners.pi yet, so we prove lemmas about functions f : M → Π i, F i and use 𝓘(𝕜, Π i, F i) as the model space.

theorem cont_mdiff_within_at_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {x : M} {n : ℕ∞} {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
cont_mdiff_within_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ s x ∀ (i : ι), cont_mdiff_within_at I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i) s x
theorem cont_mdiff_on_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {n : ℕ∞} {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
cont_mdiff_on I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ s ∀ (i : ι), cont_mdiff_on I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i) s
theorem cont_mdiff_at_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {n : ℕ∞} {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
cont_mdiff_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ x ∀ (i : ι), cont_mdiff_at I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i) x
theorem cont_mdiff_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {n : ℕ∞} {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
cont_mdiff I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ ∀ (i : ι), cont_mdiff I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i)
theorem smooth_within_at_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {x : M} {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
smooth_within_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ s x ∀ (i : ι), smooth_within_at I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i) s x
theorem smooth_on_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
smooth_on I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ s ∀ (i : ι), smooth_on I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i) s
theorem smooth_at_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
smooth_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ x ∀ (i : ι), smooth_at I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i) x
theorem smooth_pi_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {ι : Type u_14} [fintype ι] {Fi : ι → Type u_15} [Π (i : ι), normed_add_comm_group (Fi i)] [Π (i : ι), normed_space 𝕜 (Fi i)] {φ : M → Π (i : ι), Fi i} :
smooth I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ ∀ (i : ι), smooth I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i)

Linear maps between normed spaces are smooth #

theorem continuous_linear_map.cont_mdiff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_8} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} (L : E →L[𝕜] F) :

Smoothness of standard operations #

theorem smooth_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] :
smooth ((model_with_corners_self 𝕜 𝕜).prod (model_with_corners_self 𝕜 V)) (model_with_corners_self 𝕜 V) (λ (p : 𝕜 × V), p.fst p.snd)

On any vector space, multiplication by a scalar is a smooth operation.

theorem cont_mdiff_within_at.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {x : M} {n : ℕ∞} {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 𝕜) n f s x) (hg : cont_mdiff_within_at I (model_with_corners_self 𝕜 V) n g s x) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 V) n (λ (p : M), f p g p) s x
theorem cont_mdiff_at.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {n : ℕ∞} {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : cont_mdiff_at I (model_with_corners_self 𝕜 𝕜) n f x) (hg : cont_mdiff_at I (model_with_corners_self 𝕜 V) n g x) :
cont_mdiff_at I (model_with_corners_self 𝕜 V) n (λ (p : M), f p g p) x
theorem cont_mdiff_on.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {n : ℕ∞} {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : cont_mdiff_on I (model_with_corners_self 𝕜 𝕜) n f s) (hg : cont_mdiff_on I (model_with_corners_self 𝕜 V) n g s) :
cont_mdiff_on I (model_with_corners_self 𝕜 V) n (λ (p : M), f p g p) s
theorem cont_mdiff.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {n : ℕ∞} {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : cont_mdiff I (model_with_corners_self 𝕜 𝕜) n f) (hg : cont_mdiff I (model_with_corners_self 𝕜 V) n g) :
cont_mdiff I (model_with_corners_self 𝕜 V) n (λ (p : M), f p g p)
theorem smooth_within_at.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {x : M} {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : smooth_within_at I (model_with_corners_self 𝕜 𝕜) f s x) (hg : smooth_within_at I (model_with_corners_self 𝕜 V) g s x) :
smooth_within_at I (model_with_corners_self 𝕜 V) (λ (p : M), f p g p) s x
theorem smooth_at.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : smooth_at I (model_with_corners_self 𝕜 𝕜) f x) (hg : smooth_at I (model_with_corners_self 𝕜 V) g x) :
smooth_at I (model_with_corners_self 𝕜 V) (λ (p : M), f p g p) x
theorem smooth_on.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : smooth_on I (model_with_corners_self 𝕜 𝕜) f s) (hg : smooth_on I (model_with_corners_self 𝕜 V) g s) :
smooth_on I (model_with_corners_self 𝕜 V) (λ (p : M), f p g p) s
theorem smooth.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {V : Type u_14} [normed_add_comm_group V] [normed_space 𝕜 V] {f : M → 𝕜} {g : M → V} (hf : smooth I (model_with_corners_self 𝕜 𝕜) f) (hg : smooth I (model_with_corners_self 𝕜 V) g) :
smooth I (model_with_corners_self 𝕜 V) (λ (p : M), f p g p)