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'.
times_cont_mdiff_within_at I I' n f s xstates that the functionfisCⁿwithin the setsaround the pointx.times_cont_mdiff_at I I' n f xstates that the functionfisCⁿaroundx.times_cont_mdiff_on I I' n f sstates that the functionfisCⁿon the setstimes_cont_mdiff I I' n fstates that the functionfisCⁿ.times_cont_mdiff_on.compgives the invariance of theCⁿproperty under compositiontimes_cont_mdiff_on.times_cont_mdiff_on_tangent_map_withinstates that the bundled derivative of aCⁿfunction in a domain isCᵐwhenm + 1 ≤ n.times_cont_mdiff.times_cont_mdiff_tangent_mapstates that the bundled derivative of aCⁿfunction isCᵐwhenm + 1 ≤ n.times_cont_mdiff_iff_times_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 times_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 times_cont_mdiff_on_iff and times_cont_mdiff_iff.
Definition of smooth functions between manifolds
def
times_cont_diff_within_at_prop
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H'] :
model_with_corners 𝕜 E' H' → with_top ℕ → (H → H') → set H → 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
times_cont_diff_within_at_local_invariant_prop
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(n : with_top ℕ) :
Being Cⁿ in the model space is a local property, invariant under smooth maps. Therefore,
it will lift nicely to manifolds.
theorem
times_cont_diff_within_at_local_invariant_prop_mono
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(n : with_top ℕ)
⦃s : set H⦄
⦃x : H⦄
⦃t : set H⦄
⦃f : H → H'⦄ :
t ⊆ s → times_cont_diff_within_at_prop I I' n f s x → times_cont_diff_within_at_prop I I' n f t x
theorem
times_cont_diff_within_at_local_invariant_prop_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(x : H) :
def
times_cont_mdiff_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
A function is n times continuously differentiable within a set at a point in a manifold if
it is continuous and it is n times continuously differentiable in this set around this point, when
read in the preferred chart at this point.
Equations
- times_cont_mdiff_within_at I I' n f s x = charted_space.lift_prop_within_at (times_cont_diff_within_at_prop I I' n) f s x
def
smooth_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
(M → M') → set M → M → Prop
Abbreviation for times_cont_mdiff_within_at I I' ⊤ f s x. See also documentation for smooth.
Equations
- smooth_within_at I I' f s x = times_cont_mdiff_within_at I I' ⊤ f s x
def
times_cont_mdiff_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
A function is n times continuously differentiable at a point in a manifold if
it is continuous and it is n times continuously differentiable around this point, when
read in the preferred chart at this point.
Equations
- times_cont_mdiff_at I I' n f x = times_cont_mdiff_within_at I I' n f set.univ x
def
smooth_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
(M → M') → M → Prop
Abbreviation for times_cont_mdiff_at I I' ⊤ f x. See also documentation for smooth.
Equations
- smooth_at I I' f x = times_cont_mdiff_at I I' ⊤ f x
def
times_cont_mdiff_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
A function is n times continuously differentiable in a set of a manifold if it is continuous
and, for any pair of points, it is n times continuously differentiable on this set in the charts
around these points.
Equations
- times_cont_mdiff_on I I' n f s = ∀ (x : M), x ∈ s → times_cont_mdiff_within_at I I' n f s x
def
smooth_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
(M → M') → set M → Prop
Abbreviation for times_cont_mdiff_on I I' ⊤ f s. See also documentation for smooth.
Equations
- smooth_on I I' f s = times_cont_mdiff_on I I' ⊤ f s
def
times_cont_mdiff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
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
- times_cont_mdiff I I' n f = ∀ (x : M), times_cont_mdiff_at I I' n f x
def
smooth
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M'] :
(M → M') → Prop
Abbreviation for times_cont_mdiff I I' ⊤ f.
Short note to work with these abbreviations: a lemma of the form times_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 times_cont_diff, it is still better to restate
the lemma replacing times_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 = times_cont_mdiff I I' ⊤ f
Basic properties of smooth functions between manifolds
theorem
times_cont_mdiff.smooth
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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'} :
times_cont_mdiff I I' ⊤ f → smooth I I' f
theorem
smooth.times_cont_mdiff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 → times_cont_mdiff I I' ⊤ f
theorem
times_cont_mdiff_on.smooth_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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} :
times_cont_mdiff_on I I' ⊤ f s → smooth_on I I' f s
theorem
smooth_on.times_cont_mdiff_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 → times_cont_mdiff_on I I' ⊤ f s
theorem
times_cont_mdiff_at.smooth_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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} :
times_cont_mdiff_at I I' ⊤ f x → smooth_at I I' f x
theorem
smooth_at.times_cont_mdiff_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 → times_cont_mdiff_at I I' ⊤ f x
theorem
times_cont_mdiff_within_at.smooth_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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} :
times_cont_mdiff_within_at I I' ⊤ f s x → smooth_within_at I I' f s x
theorem
smooth_within_at.times_cont_mdiff_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 → times_cont_mdiff_within_at I I' ⊤ f s x
theorem
times_cont_mdiff.times_cont_mdiff_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f → times_cont_mdiff_at I I' n f x
theorem
smooth.smooth_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
times_cont_mdiff_within_at_univ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f set.univ x ↔ times_cont_mdiff_at I I' n f x
theorem
smooth_at_univ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
times_cont_mdiff_on_univ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f set.univ ↔ times_cont_mdiff I I' n f
theorem
smooth_on_univ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
times_cont_mdiff_within_at_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ times_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.
theorem
smooth_within_at_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 ∧ times_cont_diff_within_at 𝕜 ⊤ (⇑(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)
theorem
times_cont_mdiff_on_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s ↔ continuous_on f s ∧ ∀ (x : M) (y : M'), times_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
smooth_on_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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'), times_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
times_cont_mdiff_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f ↔ continuous f ∧ ∀ (x : M) (y : M'), times_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
smooth_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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'), times_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))
Deducing smoothness from higher smoothness
theorem
times_cont_mdiff_within_at.of_le
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x → m ≤ n → times_cont_mdiff_within_at I I' m f s x
theorem
times_cont_mdiff_at.of_le
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_at I I' n f x → m ≤ n → times_cont_mdiff_at I I' m f x
theorem
times_cont_mdiff_on.of_le
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s → m ≤ n → times_cont_mdiff_on I I' m f s
theorem
times_cont_mdiff.of_le
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f → m ≤ n → times_cont_mdiff I I' m f
Deducing smoothness from smoothness one step beyond
theorem
times_cont_mdiff_within_at.of_succ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ} :
times_cont_mdiff_within_at I I' ↑(n.succ) f s x → times_cont_mdiff_within_at I I' ↑n f s x
theorem
times_cont_mdiff_at.of_succ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ} :
times_cont_mdiff_at I I' ↑(n.succ) f x → times_cont_mdiff_at I I' ↑n f x
theorem
times_cont_mdiff_on.of_succ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ} :
times_cont_mdiff_on I I' ↑(n.succ) f s → times_cont_mdiff_on I I' ↑n f s
theorem
times_cont_mdiff.of_succ
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ} :
times_cont_mdiff I I' ↑(n.succ) f → times_cont_mdiff I I' ↑n f
Deducing continuity from smoothness
theorem
times_cont_mdiff_within_at.continuous_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x → continuous_within_at f s x
theorem
times_cont_mdiff_at.continuous_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_at I I' n f x → continuous_at f x
theorem
times_cont_mdiff_on.continuous_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s → continuous_on f s
theorem
times_cont_mdiff.continuous
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f → continuous f
Deducing differentiability from smoothness
theorem
times_cont_mdiff_within_at.mdifferentiable_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x → 1 ≤ n → mdifferentiable_within_at I I' f s x
theorem
times_cont_mdiff_at.mdifferentiable_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_at I I' n f x → 1 ≤ n → mdifferentiable_at I I' f x
theorem
times_cont_mdiff_on.mdifferentiable_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s → 1 ≤ n → mdifferentiable_on I I' f s
theorem
times_cont_mdiff.mdifferentiable
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f → 1 ≤ n → mdifferentiable I I' f
C^∞ smoothness
theorem
times_cont_mdiff_within_at_top
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ), times_cont_mdiff_within_at I I' ↑n f s x
theorem
times_cont_mdiff_at_top
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ), times_cont_mdiff_at I I' ↑n f x
theorem
times_cont_mdiff_on_top
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ), times_cont_mdiff_on I I' ↑n f s
theorem
times_cont_mdiff_top
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ), times_cont_mdiff I I' ↑n f
theorem
times_cont_mdiff_within_at_iff_nat
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x ↔ ∀ (m : ℕ), ↑m ≤ n → times_cont_mdiff_within_at I I' ↑m f s x
Restriction to a smaller set
theorem
times_cont_mdiff_within_at.mono
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x → t ⊆ s → times_cont_mdiff_within_at I I' n f t x
theorem
times_cont_mdiff_at.times_cont_mdiff_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_at I I' n f x → times_cont_mdiff_within_at I I' n f s x
theorem
smooth_at.smooth_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_at I I' f x → smooth_within_at I I' f s x
theorem
times_cont_mdiff_on.mono
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s → t ⊆ s → times_cont_mdiff_on I I' n f t
theorem
times_cont_mdiff.times_cont_mdiff_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f → times_cont_mdiff_on I I' n f s
theorem
smooth.smooth_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
times_cont_mdiff_within_at_inter'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
t ∈ nhds_within x s → (times_cont_mdiff_within_at I I' n f (s ∩ t) x ↔ times_cont_mdiff_within_at I I' n f s x)
theorem
times_cont_mdiff_within_at_inter
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
t ∈ nhds x → (times_cont_mdiff_within_at I I' n f (s ∩ t) x ↔ times_cont_mdiff_within_at I I' n f s x)
theorem
times_cont_mdiff_within_at.times_cont_mdiff_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x → s ∈ nhds x → times_cont_mdiff_at I I' n f x
theorem
smooth_within_at.smooth_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 → s ∈ nhds x → smooth_at I I' f x
theorem
times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ} :
times_cont_mdiff_within_at I I' ↑n f s x ↔ ∃ (u : set M) (H_1 : u ∈ nhds_within x (has_insert.insert x s)), times_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
times_cont_mdiff_at_iff_times_cont_mdiff_on_nhds
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : ℕ} :
times_cont_mdiff_at I I' ↑n f x ↔ ∃ (u : set M) (H_1 : u ∈ nhds x), times_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.
Congruence lemmas
theorem
times_cont_mdiff_within_at.congr
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x → (∀ (y : M), y ∈ s → f₁ y = f y) → f₁ x = f x → times_cont_mdiff_within_at I I' n f₁ s x
theorem
times_cont_mdiff_within_at_congr
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
(∀ (y : M), y ∈ s → f₁ y = f y) → f₁ x = f x → (times_cont_mdiff_within_at I I' n f₁ s x ↔ times_cont_mdiff_within_at I I' n f s x)
theorem
times_cont_mdiff_within_at.congr_of_eventually_eq
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I' n f s x → f₁ =ᶠ[nhds_within x s] f → f₁ x = f x → times_cont_mdiff_within_at I I' n f₁ s x
theorem
filter.eventually_eq.times_cont_mdiff_within_at_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
f₁ =ᶠ[nhds_within x s] f → f₁ x = f x → (times_cont_mdiff_within_at I I' n f₁ s x ↔ times_cont_mdiff_within_at I I' n f s x)
theorem
times_cont_mdiff_at.congr_of_eventually_eq
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_at I I' n f x → f₁ =ᶠ[nhds x] f → times_cont_mdiff_at I I' n f₁ x
theorem
filter.eventually_eq.times_cont_mdiff_at_iff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
f₁ =ᶠ[nhds x] f → (times_cont_mdiff_at I I' n f₁ x ↔ times_cont_mdiff_at I I' n f x)
theorem
times_cont_mdiff_on.congr
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s → (∀ (y : M), y ∈ s → f₁ y = f y) → times_cont_mdiff_on I I' n f₁ s
theorem
times_cont_mdiff_on_congr
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
(∀ (y : M), y ∈ s → f₁ y = f y) → (times_cont_mdiff_on I I' n f₁ s ↔ times_cont_mdiff_on I I' n f s)
Locality
theorem
times_cont_mdiff_on_of_locally_times_cont_mdiff_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
(∀ (x : M), x ∈ s → (∃ (u : set M), is_open u ∧ x ∈ u ∧ times_cont_mdiff_on I I' n f (s ∩ u))) → times_cont_mdiff_on I I' n f s
Being C^n is a local property.
theorem
times_cont_mdiff_of_locally_times_cont_mdiff_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
(∀ (x : M), ∃ (u : set M), is_open u ∧ x ∈ u ∧ times_cont_mdiff_on I I' n f u) → times_cont_mdiff I I' n f
Smoothness of the composition of smooth functions between manifolds
theorem
times_cont_mdiff_on.comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{E'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{t : set M'}
{g : M' → M''} :
times_cont_mdiff_on I' I'' n g t → times_cont_mdiff_on I I' n f s → s ⊆ f ⁻¹' t → times_cont_mdiff_on I I'' n (g ∘ f) s
The composition of C^n functions on domains is C^n.
theorem
times_cont_mdiff_on.comp'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{E'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{t : set M'}
{g : M' → M''} :
times_cont_mdiff_on I' I'' n g t → times_cont_mdiff_on I I' n f s → times_cont_mdiff_on I I'' n (g ∘ f) (s ∩ f ⁻¹' t)
The composition of C^n functions on domains is C^n.
theorem
times_cont_mdiff.comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{E'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{g : M' → M''} :
times_cont_mdiff I' I'' n g → times_cont_mdiff I I' n f → times_cont_mdiff I I'' n (g ∘ f)
The composition of C^n functions is C^n.
theorem
times_cont_mdiff_within_at.comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{E'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{t : set M'}
{g : M' → M''}
(x : M) :
times_cont_mdiff_within_at I' I'' n g t (f x) → times_cont_mdiff_within_at I I' n f s x → s ⊆ f ⁻¹' t → times_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
times_cont_mdiff_within_at.comp'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{E'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{t : set M'}
{g : M' → M''}
(x : M) :
times_cont_mdiff_within_at I' I'' n g t (f x) → times_cont_mdiff_within_at I I' n f s x → times_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
times_cont_mdiff_at.comp
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{E'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{g : M' → M''}
(x : M) :
times_cont_mdiff_at I' I'' n g (f x) → times_cont_mdiff_at I I' n f x → times_cont_mdiff_at I I'' n (g ∘ f) x
The composition of C^n functions at points is C^n.
theorem
times_cont_mdiff.comp_times_cont_mdiff_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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']
{n : with_top ℕ}
{E'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{f : M → M'}
{g : M' → M''}
{s : set M} :
times_cont_mdiff I' I'' n g → times_cont_mdiff_on I I' n f s → times_cont_mdiff_on I I'' n (g ∘ f) s
theorem
smooth.comp_smooth_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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'' : Type u_14}
[normed_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'']
[smooth_manifold_with_corners I'' M'']
{f : M → M'}
{g : M' → M''}
{s : set M} :
Atlas members are smooth
theorem
times_cont_mdiff_on_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ}
{e : local_homeomorph M H} :
e ∈ smooth_manifold_with_corners.maximal_atlas I M → times_cont_mdiff_on I I n ⇑e e.to_local_equiv.source
An atlas member is C^n for any n.
theorem
times_cont_mdiff_on_symm_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ}
{e : local_homeomorph M H} :
e ∈ smooth_manifold_with_corners.maximal_atlas I M → times_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
times_cont_mdiff_on_chart
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ} :
times_cont_mdiff_on I I n ⇑(charted_space.chart_at H x) (charted_space.chart_at H x).to_local_equiv.source
theorem
times_cont_mdiff_on_chart_symm
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ} :
times_cont_mdiff_on I I n ⇑((charted_space.chart_at H x).symm) (charted_space.chart_at H x).to_local_equiv.target
The identity is smooth
theorem
times_cont_mdiff_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ} :
times_cont_mdiff I I n id
theorem
smooth_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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
times_cont_mdiff_on_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ} :
times_cont_mdiff_on I I n id s
theorem
smooth_on_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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
times_cont_mdiff_at_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ} :
times_cont_mdiff_at I I n id x
theorem
smooth_at_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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
times_cont_mdiff_within_at_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ} :
times_cont_mdiff_within_at I I n id s x
theorem
smooth_within_at_id
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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} :
smooth_within_at I I id s x
Constants are smooth
theorem
times_cont_mdiff_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{c : M'} :
times_cont_mdiff I I' n (λ (x : M), c)
theorem
smooth_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
times_cont_mdiff_on_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{c : M'} :
times_cont_mdiff_on I I' n (λ (x : M), c) s
theorem
smooth_on_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
times_cont_mdiff_at_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{c : M'} :
times_cont_mdiff_at I I' n (λ (x : M), c) x
theorem
smooth_at_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
times_cont_mdiff_within_at_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ}
{c : M'} :
times_cont_mdiff_within_at I I' n (λ (x : M), c) s x
theorem
smooth_within_at_const
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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
Equivalence with the basic definition for functions between vector spaces
theorem
times_cont_mdiff_within_at_iff_times_cont_diff_within_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
{f : E → E'}
{s : set E}
{x : E} :
times_cont_mdiff_within_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s x ↔ times_cont_diff_within_at 𝕜 n f s x
theorem
times_cont_mdiff_at_iff_times_cont_diff_at
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
{f : E → E'}
{x : E} :
times_cont_mdiff_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f x ↔ times_cont_diff_at 𝕜 n f x
theorem
times_cont_mdiff_on_iff_times_cont_diff_on
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
{f : E → E'}
{s : set E} :
times_cont_mdiff_on (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s ↔ times_cont_diff_on 𝕜 n f s
theorem
times_cont_mdiff_iff_times_cont_diff
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
{f : E → E'} :
times_cont_mdiff (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f ↔ times_cont_diff 𝕜 n f
The tangent map of a smooth function is smooth
theorem
times_cont_mdiff_on.continuous_on_tangent_map_within_aux
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{n : with_top ℕ}
{f : H → H'}
{s : set H} :
times_cont_mdiff_on I I' n f s → 1 ≤ n → unique_mdiff_on I s → continuous_on (tangent_map_within I I' f s) (tangent_bundle.proj I H ⁻¹' 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
times_cont_mdiff_on.continuous_on_tangent_map_within
theorem
times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within_aux
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{E' : Type u_5}
[normed_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{m n : with_top ℕ}
{f : H → H'}
{s : set H} :
times_cont_mdiff_on I I' n f s → m + 1 ≤ n → unique_mdiff_on I s → times_cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s) (tangent_bundle.proj I H ⁻¹' 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
times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within
theorem
times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s → m + 1 ≤ n → unique_mdiff_on I s → times_cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s) (tangent_bundle.proj I M ⁻¹' 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
times_cont_mdiff_on.continuous_on_tangent_map_within
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff_on I I' n f s → 1 ≤ n → unique_mdiff_on I s → continuous_on (tangent_map_within I I' f s) (tangent_bundle.proj I M ⁻¹' s)
If a function is C^n on a domain with unique derivatives, with 1 ≤ n, then its bundled
derivative is continuous there.
theorem
times_cont_mdiff.times_cont_mdiff_tangent_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f → m + 1 ≤ n → times_cont_mdiff I.tangent I'.tangent m (tangent_map I I' f)
If a function is C^n, then its bundled derivative is C^m when m+1 ≤ n.
theorem
times_cont_mdiff.continuous_tangent_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : with_top ℕ} :
times_cont_mdiff I I' n f → 1 ≤ n → continuous (tangent_map I I' f)
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_bundle_core.times_cont_mdiff_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
(Z : basic_smooth_bundle_core I M E') :
times_cont_mdiff (I.prod (model_with_corners_self 𝕜 E')) I n Z.to_topological_fiber_bundle_core.proj
theorem
basic_smooth_bundle_core.smooth_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
(Z : basic_smooth_bundle_core I M E') :
smooth (I.prod (model_with_corners_self 𝕜 E')) I Z.to_topological_fiber_bundle_core.proj
theorem
basic_smooth_bundle_core.times_cont_mdiff_on_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
(Z : basic_smooth_bundle_core I M E')
{s : set Z.to_topological_fiber_bundle_core.total_space} :
times_cont_mdiff_on (I.prod (model_with_corners_self 𝕜 E')) I n Z.to_topological_fiber_bundle_core.proj s
theorem
basic_smooth_bundle_core.smooth_on_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
(Z : basic_smooth_bundle_core I M E')
{s : set Z.to_topological_fiber_bundle_core.total_space} :
smooth_on (I.prod (model_with_corners_self 𝕜 E')) I Z.to_topological_fiber_bundle_core.proj s
theorem
basic_smooth_bundle_core.times_cont_mdiff_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
(Z : basic_smooth_bundle_core I M E')
{p : Z.to_topological_fiber_bundle_core.total_space} :
times_cont_mdiff_at (I.prod (model_with_corners_self 𝕜 E')) I n Z.to_topological_fiber_bundle_core.proj p
theorem
basic_smooth_bundle_core.smooth_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
(Z : basic_smooth_bundle_core I M E')
{p : Z.to_topological_fiber_bundle_core.total_space} :
smooth_at (I.prod (model_with_corners_self 𝕜 E')) I Z.to_topological_fiber_bundle_core.proj p
theorem
basic_smooth_bundle_core.times_cont_mdiff_within_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{n : with_top ℕ}
(Z : basic_smooth_bundle_core I M E')
{s : set Z.to_topological_fiber_bundle_core.total_space}
{p : Z.to_topological_fiber_bundle_core.total_space} :
times_cont_mdiff_within_at (I.prod (model_with_corners_self 𝕜 E')) I n Z.to_topological_fiber_bundle_core.proj s p
theorem
basic_smooth_bundle_core.smooth_within_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
(Z : basic_smooth_bundle_core I M E')
{s : set Z.to_topological_fiber_bundle_core.total_space}
{p : Z.to_topological_fiber_bundle_core.total_space} :
smooth_within_at (I.prod (model_with_corners_self 𝕜 E')) I Z.to_topological_fiber_bundle_core.proj s p
Smoothness of the tangent bundle projection
theorem
tangent_bundle.times_cont_mdiff_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ} :
times_cont_mdiff I.tangent I n (tangent_bundle.proj I M)
theorem
tangent_bundle.smooth_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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] :
smooth I.tangent I (tangent_bundle.proj I M)
theorem
tangent_bundle.times_cont_mdiff_on_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ}
{s : set (tangent_bundle I M)} :
times_cont_mdiff_on I.tangent I n (tangent_bundle.proj I M) s
theorem
tangent_bundle.smooth_on_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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)} :
smooth_on I.tangent I (tangent_bundle.proj I M) s
theorem
tangent_bundle.times_cont_mdiff_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ}
{p : tangent_bundle I M} :
times_cont_mdiff_at I.tangent I n (tangent_bundle.proj I M) p
theorem
tangent_bundle.smooth_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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} :
smooth_at I.tangent I (tangent_bundle.proj I M) p
theorem
tangent_bundle.times_cont_mdiff_within_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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 : with_top ℕ}
{s : set (tangent_bundle I M)}
{p : tangent_bundle I M} :
times_cont_mdiff_within_at I.tangent I n (tangent_bundle.proj I M) s p
theorem
tangent_bundle.smooth_within_at_proj
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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} :
smooth_within_at I.tangent I (tangent_bundle.proj I M) s p
Smoothness of standard maps associated to the product of manifolds
theorem
times_cont_mdiff_within_at.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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 : with_top ℕ}
{f : M → M'}
{g : M → N'} :
times_cont_mdiff_within_at I I' n f s x → times_cont_mdiff_within_at I J' n g s x → times_cont_mdiff_within_at I (I'.prod J') n (λ (x : M), (f x, g x)) s x
theorem
times_cont_mdiff_at.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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 : with_top ℕ}
{f : M → M'}
{g : M → N'} :
times_cont_mdiff_at I I' n f x → times_cont_mdiff_at I J' n g x → times_cont_mdiff_at I (I'.prod J') n (λ (x : M), (f x, g x)) x
theorem
times_cont_mdiff_on.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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 : with_top ℕ}
{f : M → M'}
{g : M → N'} :
times_cont_mdiff_on I I' n f s → times_cont_mdiff_on I J' n g s → times_cont_mdiff_on I (I'.prod J') n (λ (x : M), (f x, g x)) s
theorem
times_cont_mdiff.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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 : with_top ℕ}
{f : M → M'}
{g : M → N'} :
times_cont_mdiff I I' n f → times_cont_mdiff I J' n g → times_cont_mdiff I (I'.prod J') n (λ (x : M), (f x, g x))
theorem
smooth_within_at.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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'} :
smooth_within_at I I' f s x → 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_at.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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'} :
theorem
smooth_on.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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'} :
theorem
smooth.prod_mk
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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_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'} :
theorem
times_cont_mdiff_within_at_fst
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ}
{s : set (M × N)}
{p : M × N} :
times_cont_mdiff_within_at (I.prod J) I n prod.fst s p
theorem
times_cont_mdiff_at_fst
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ}
{p : M × N} :
times_cont_mdiff_at (I.prod J) I n prod.fst p
theorem
times_cont_mdiff_on_fst
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ}
{s : set (M × N)} :
times_cont_mdiff_on (I.prod J) I n prod.fst s
theorem
times_cont_mdiff_fst
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ} :
times_cont_mdiff (I.prod J) I n prod.fst
theorem
smooth_within_at_fst
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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} :
smooth_within_at (I.prod J) I prod.fst s p
theorem
smooth_at_fst
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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
times_cont_mdiff_within_at_snd
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ}
{s : set (M × N)}
{p : M × N} :
times_cont_mdiff_within_at (I.prod J) J n prod.snd s p
theorem
times_cont_mdiff_at_snd
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ}
{p : M × N} :
times_cont_mdiff_at (I.prod J) J n prod.snd p
theorem
times_cont_mdiff_on_snd
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ}
{s : set (M × N)} :
times_cont_mdiff_on (I.prod J) J n prod.snd s
theorem
times_cont_mdiff_snd
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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 : with_top ℕ} :
times_cont_mdiff (I.prod J) J n prod.snd
theorem
smooth_within_at_snd
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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} :
smooth_within_at (I.prod J) J prod.snd s p
theorem
smooth_at_snd
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_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}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M' × N'} :
theorem
times_cont_mdiff_within_at.prod_map'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{s : set M}
{n : with_top ℕ}
{g : N → N'}
{r : set N}
{p : M × N} :
times_cont_mdiff_within_at I I' n f s p.fst → times_cont_mdiff_within_at J J' n g r p.snd → times_cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s.prod 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
times_cont_mdiff_within_at.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{s : set M}
{x : M}
{n : with_top ℕ}
{g : N → N'}
{r : set N}
{y : N} :
times_cont_mdiff_within_at I I' n f s x → times_cont_mdiff_within_at J J' n g r y → times_cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s.prod r) (x, y)
theorem
times_cont_mdiff_at.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{x : M}
{n : with_top ℕ}
{g : N → N'}
{y : N} :
times_cont_mdiff_at I I' n f x → times_cont_mdiff_at J J' n g y → times_cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) (x, y)
theorem
times_cont_mdiff_at.prod_map'
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{n : with_top ℕ}
{g : N → N'}
{p : M × N} :
times_cont_mdiff_at I I' n f p.fst → times_cont_mdiff_at J J' n g p.snd → times_cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) p
theorem
times_cont_mdiff_on.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{s : set M}
{n : with_top ℕ}
{g : N → N'}
{r : set N} :
times_cont_mdiff_on I I' n f s → times_cont_mdiff_on J J' n g r → times_cont_mdiff_on (I.prod J) (I'.prod J') n (prod.map f g) (s.prod r)
theorem
times_cont_mdiff.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{n : with_top ℕ}
{g : N → N'} :
times_cont_mdiff I I' n f → times_cont_mdiff J J' n g → times_cont_mdiff (I.prod J) (I'.prod J') n (prod.map f g)
theorem
smooth_within_at.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{s : set M}
{x : M}
{g : N → N'}
{r : set N}
{y : N} :
smooth_within_at I I' f s x → smooth_within_at J J' g r y → smooth_within_at (I.prod J) (I'.prod J') (prod.map f g) (s.prod r) (x, y)
theorem
smooth_at.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{x : M}
{g : N → N'}
{y : N} :
theorem
smooth_on.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{s : set M}
{g : N → N'}
{r : set N} :
theorem
smooth.prod_map
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{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_group E']
[normed_space 𝕜 E']
{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 : Type u_8}
[normed_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]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_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']
[J's : smooth_manifold_with_corners J' N']
{f : M → M'}
{g : N → N'} :