Smooth functions between smooth manifolds #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define Cⁿ functions between smooth manifolds, as functions which are Cⁿ in charts, and prove
basic properties of these notions.
Main definitions and statements #
Let M and M' be two smooth manifolds, with respect to model with corners I and I'. Let
f : M → M'.
cont_mdiff_within_at I I' n f s xstates that the functionfisCⁿwithin the setsaround the pointx.cont_mdiff_at I I' n f xstates that the functionfisCⁿaroundx.cont_mdiff_on I I' n f sstates that the functionfisCⁿon the setscont_mdiff I I' n fstates that the functionfisCⁿ.cont_mdiff_on.compgives the invariance of theCⁿproperty under compositioncont_mdiff_iff_cont_diffstates that, for functions between vector spaces, manifold-smoothness is equivalent to usual smoothness.
We also give many basic properties of smooth functions between manifolds, following the API of smooth functions between vector spaces.
Implementation details #
Many properties follow for free from the corresponding properties of functions in vector spaces,
as being Cⁿ is a local property invariant under the smooth groupoid. We take advantage of the
general machinery developed in local_invariant_properties.lean to get these properties
automatically. For instance, the fact that being Cⁿ does not depend on the chart one considers
is given by lift_prop_within_at_indep_chart.
For this to work, the definition of cont_mdiff_within_at and friends has to
follow definitionally the setup of local invariant properties. Still, we recast the definition
in terms of extended charts in cont_mdiff_on_iff and cont_mdiff_iff.
Definition of smooth functions between manifolds #
def
cont_diff_within_at_prop
{𝕜 : Type u_1}
[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.
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} :
cont_diff_within_at_prop (model_with_corners_self 𝕜 E) I' n f s x ↔ cont_diff_within_at 𝕜 n (⇑I' ∘ f) s x
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} :
cont_diff_within_at_prop (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s x ↔ cont_diff_within_at 𝕜 n f s x
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} :
cont_diff_within_at_prop I (model_with_corners_self 𝕜 E') n f s x ↔ cont_diff_within_at 𝕜 n (f ∘ ⇑(I.symm)) (⇑(I.symm) ⁻¹' s ∩ set.range ⇑I) (⇑I x)
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 : ℕ∞) :
(cont_diff_groupoid ⊤ I).local_invariant_prop (cont_diff_groupoid ⊤ I') (cont_diff_within_at_prop I I' n)
Being Cⁿ in the model space is a local property, invariant under smooth maps. Therefore,
it will lift nicely to manifolds.
theorem
cont_diff_within_at_prop_mono_of_mem
{𝕜 : Type u_1}
[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 : s ∈ nhds_within x t)
(h : cont_diff_within_at_prop I I' n f s x) :
cont_diff_within_at_prop I I' n f t 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)
{n : ℕ∞}
(x : H) :
cont_diff_within_at_prop I I n id set.univ x
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
- cont_mdiff_within_at I I' n f s x = charted_space.lift_prop_within_at (cont_diff_within_at_prop I I' n) f s x
@[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
- smooth_within_at I I' f s x = cont_mdiff_within_at I I' ⊤ f s x
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
- cont_mdiff_at I I' n f x = cont_mdiff_within_at I I' n f set.univ x
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} :
cont_mdiff_at I I' n f x ↔ continuous_at f x ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (set.range ⇑I) (⇑(ext_chart_at I x) x)
@[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
- smooth_at I I' f x = cont_mdiff_at I I' ⊤ f x
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
- cont_mdiff_on I I' n f s = ∀ (x : M), x ∈ s → cont_mdiff_within_at I I' n f s x
@[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
- smooth_on I I' f s = cont_mdiff_on I I' ⊤ f s
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
- cont_mdiff I I' n f = ∀ (x : M), cont_mdiff_at I I' n f x
@[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
- smooth I I' f = cont_mdiff I I' ⊤ f
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) :
cont_mdiff 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) :
cont_mdiff_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) :
cont_mdiff_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) :
cont_mdiff_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 : ℕ∞} :
cont_mdiff_within_at I I' n f set.univ x ↔ cont_mdiff_at I I' n f x
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} :
smooth_within_at I I' f set.univ x ↔ smooth_at I I' f x
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 : ℕ∞} :
cont_mdiff_on I I' n f set.univ ↔ cont_mdiff I I' n f
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 : ℕ∞} :
cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x)
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart.
theorem
cont_mdiff_within_at_iff'
{𝕜 : Type u_1}
[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 ↔ continuous_within_at f s x ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) ((ext_chart_at I x).target ∩ ⇑((ext_chart_at I x).symm) ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' (f x)).source)) (⇑(ext_chart_at I x) x)
One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart. This form states smoothness of f
written in such a way that the set is restricted to lie within the domain/codomain of the
corresponding charts.
Even though this expression is more complicated than the one in cont_mdiff_within_at_iff, it is
a smaller set, but their germs at ext_chart_at I x x are equal. It is sometimes useful to rewrite
using this in the goal.
theorem
cont_mdiff_within_at_iff_target
{𝕜 : Type u_1}
[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 ↔ continuous_within_at f s x ∧ cont_mdiff_within_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' (f x)) ∘ f) s x
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart in the target.
theorem
smooth_within_at_iff
{𝕜 : Type u_1}
[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 ↔ continuous_within_at f s x ∧ cont_diff_within_at 𝕜 ⊤ (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x)
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} :
smooth_within_at I I' f s x ↔ continuous_within_at f s x ∧ smooth_within_at I (model_with_corners_self 𝕜 E') (⇑(ext_chart_at I' (f x)) ∘ f) s x
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} :
cont_mdiff_at I I' n f x ↔ continuous_at f x ∧ cont_mdiff_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' (f x)) ∘ f) x
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} :
smooth_at I I' f x ↔ continuous_at f x ∧ smooth_at I (model_with_corners_self 𝕜 E') (⇑(ext_chart_at I' (f x)) ∘ f) x
theorem
cont_mdiff_within_at_iff_of_mem_maximal_atlas
{𝕜 : 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']
{e : local_homeomorph M H}
{e' : local_homeomorph M' H'}
{f : M → M'}
{s : set M}
{n : ℕ∞}
{x : M}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(he' : e' ∈ smooth_manifold_with_corners.maximal_atlas I' M')
(hx : x ∈ e.to_local_equiv.source)
(hy : f x ∈ e'.to_local_equiv.source) :
theorem
cont_mdiff_within_at_iff_image
{𝕜 : 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']
{e : local_homeomorph M H}
{e' : local_homeomorph M' H'}
{f : M → M'}
{s : set M}
{n : ℕ∞}
{x : M}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(he' : e' ∈ smooth_manifold_with_corners.maximal_atlas I' M')
(hs : s ⊆ e.to_local_equiv.source)
(hx : x ∈ e.to_local_equiv.source)
(hy : f x ∈ e'.to_local_equiv.source) :
An alternative formulation of cont_mdiff_within_at_iff_of_mem_maximal_atlas
if the set if s lies in e.source.
theorem
cont_mdiff_within_at_iff_of_mem_source
{𝕜 : Type u_1}
[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) :
cont_mdiff_within_at I I' n f s x' ↔ continuous_within_at f s x' ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x')
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in any chart containing that point.
theorem
cont_mdiff_within_at_iff_of_mem_source'
{𝕜 : Type u_1}
[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) :
cont_mdiff_within_at I I' n f s x' ↔ continuous_within_at f s x' ∧ cont_diff_within_at 𝕜 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)) (⇑(ext_chart_at I x) x')
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) :
cont_mdiff_at I I' n f x' ↔ continuous_at f x' ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (set.range ⇑I) (⇑(ext_chart_at I x) x')
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) :
cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ cont_mdiff_within_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' y) ∘ f) s x
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) :
cont_mdiff_at I I' n f x ↔ continuous_at f x ∧ cont_mdiff_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' y) ∘ f) x
theorem
cont_mdiff_within_at_iff_source_of_mem_maximal_atlas
{𝕜 : 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']
{e : local_homeomorph M H}
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(hx : x ∈ e.to_local_equiv.source) :
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) :
cont_mdiff_within_at I I' n f s x' ↔ cont_mdiff_within_at (model_with_corners_self 𝕜 E) I' n (f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x')
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) :
cont_mdiff_at I I' n f x' ↔ cont_mdiff_within_at (model_with_corners_self 𝕜 E) I' n (f ∘ ⇑((ext_chart_at I x).symm)) (set.range ⇑I) (⇑(ext_chart_at I x) x')
theorem
cont_mdiff_on_iff_of_mem_maximal_atlas
{𝕜 : 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']
{e : local_homeomorph M H}
{e' : local_homeomorph M' H'}
{f : M → M'}
{s : set M}
{n : ℕ∞}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(he' : e' ∈ smooth_manifold_with_corners.maximal_atlas I' M')
(hs : s ⊆ e.to_local_equiv.source)
(h2s : set.maps_to f s e'.to_local_equiv.source) :
cont_mdiff_on I I' n f s ↔ continuous_on f s ∧ cont_diff_on 𝕜 n (⇑(e'.extend I') ∘ f ∘ ⇑((e.extend I).symm)) (⇑(e.extend I) '' s)
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) :
cont_mdiff_on I I' n f s ↔ continuous_on f s ∧ cont_diff_on 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑(ext_chart_at I x) '' s)
If the set where you want f to be smooth lies entirely in a single chart, and f maps it
into a single chart, the smoothness of f on that set can be expressed by purely looking in
these charts.
Note: this lemma uses ext_chart_at I x '' s instead of (ext_chart_at I x).symm ⁻¹' s to ensure
that this set lies in (ext_chart_at I x).target.
theorem
cont_mdiff_on_iff
{𝕜 : Type u_1}
[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) :
cont_mdiff_within_at I I' m f s x
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) :
cont_mdiff_within_at I I' ↑n 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) :
continuous_within_at 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) :
continuous_at 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) :
continuous_on 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) :
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} :
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} :
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'} :
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 ≤ n → cont_mdiff_within_at I I' ↑m f s x
Restriction to a smaller set #
theorem
cont_mdiff_within_at.mono_of_mem
{𝕜 : 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 : s ∈ nhds_within x t) :
cont_mdiff_within_at I I' n f t x
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) :
cont_mdiff_within_at I I' n f t x
theorem
cont_mdiff_within_at_congr_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]
{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 : ℕ∞}
(hst : nhds_within x s = nhds_within x t) :
cont_mdiff_within_at I I' n f s x ↔ cont_mdiff_within_at I I' n f t x
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) :
cont_mdiff_within_at I I' n f s 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_iff_source_of_mem_maximal_atlas
{𝕜 : 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']
{e : local_homeomorph M H}
{f : M → M'}
{s : set M}
{n : ℕ∞}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(hs : s ⊆ e.to_local_equiv.source) :
cont_mdiff_on I I' n f s ↔ cont_mdiff_on (model_with_corners_self 𝕜 E) I' n (f ∘ ⇑((e.extend I).symm)) (⇑(e.extend I) '' s)
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 ∈ s → f₁ 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 ∈ s → f₁ 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 ∈ s → f₁ 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 ∈ s → f₁ 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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{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_within_at.comp_of_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{t : set M'}
{g : M' → M''}
{x : M}
{y : M'}
(hg : cont_mdiff_within_at I' I'' n g t y)
(hf : cont_mdiff_within_at I I' n f s x)
(st : set.maps_to f s t)
(hx : f x = y) :
cont_mdiff_within_at I I'' n (g ∘ f) s x
theorem
smooth_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(x : M)
(hg : smooth_within_at I' I'' g t (f x))
(hf : smooth_within_at I I' f s x)
(st : set.maps_to f s t) :
smooth_within_at I I'' (g ∘ f) s x
The composition of C^∞ functions within domains at points is C^∞.
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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{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
smooth_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(hg : smooth_on I' I'' g t)
(hf : smooth_on I I' f s)
(st : s ⊆ f ⁻¹' t) :
The composition of C^∞ functions on domains is C^∞.
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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{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
smooth_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(hg : smooth_on I' I'' g t)
(hf : smooth_on I I' f s) :
The composition of C^∞ functions is C^∞.
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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{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
smooth.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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{g : M' → M''}
(hg : smooth I' I'' g)
(hf : smooth I I' f) :
The composition of C^∞ functions is C^∞.
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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{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
smooth_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(x : M)
(hg : smooth_within_at I' I'' g t (f x))
(hf : smooth_within_at I I' f s x) :
smooth_within_at I I'' (g ∘ f) (s ∩ f ⁻¹' t) x
The composition of C^∞ functions within domains at points is C^∞.
theorem
cont_mdiff_at.comp_cont_mdiff_within_at
{𝕜 : Type u_1}
[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_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{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
smooth_at.comp_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{g : M' → M''}
(x : M)
(hg : smooth_at I' I'' g (f x))
(hf : smooth_within_at I I' f s x) :
smooth_within_at I I'' (g ∘ f) s x
g ∘ f is C^∞ within s at x if g is C^∞ at f x and
f is C^∞ within s at x.
theorem
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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{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_at.comp_of_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{g : M' → M''}
{x : M}
{y : M'}
(hg : cont_mdiff_at I' I'' n g y)
(hf : cont_mdiff_at I I' n f x)
(hx : f x = y) :
cont_mdiff_at I I'' n (g ∘ f) x
theorem
smooth_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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{g : M' → M''}
(x : M)
(hg : smooth_at I' I'' g (f x))
(hf : smooth_at I I' f x) :
The composition of C^∞ functions at points is C^∞.
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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{n : ℕ∞}
{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_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[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) :
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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{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']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → 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) :
Atlas members are smooth #
theorem
cont_mdiff_model
{𝕜 : 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}
{n : ℕ∞} :
cont_mdiff I (model_with_corners_self 𝕜 E) n ⇑I
theorem
cont_mdiff_on_model_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}
{n : ℕ∞} :
cont_mdiff_on (model_with_corners_self 𝕜 E) I n ⇑(I.symm) (set.range ⇑I)
theorem
cont_mdiff_on_of_mem_maximal_atlas
{𝕜 : 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 : local_homeomorph M H}
{n : ℕ∞}
(h : e ∈ smooth_manifold_with_corners.maximal_atlas I M) :
cont_mdiff_on I I n ⇑e e.to_local_equiv.source
An atlas member is C^n for any n.
theorem
cont_mdiff_on_symm_of_mem_maximal_atlas
{𝕜 : 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 : local_homeomorph M H}
{n : ℕ∞}
(h : e ∈ smooth_manifold_with_corners.maximal_atlas I M) :
cont_mdiff_on I I n ⇑(e.symm) e.to_local_equiv.target
The inverse of an atlas member is C^n for any n.
theorem
cont_mdiff_at_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜