Smooth functions between smooth manifolds #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define Cⁿ functions between smooth manifolds, as functions which are Cⁿ in charts, and prove
basic properties of these notions.
Main definitions and statements #
Let M and M' be two smooth manifolds, with respect to model with corners I and I'. Let
f : M → M'.
cont_mdiff_within_at I I' n f s xstates that the functionfisCⁿwithin the setsaround the pointx.cont_mdiff_at I I' n f xstates that the functionfisCⁿaroundx.cont_mdiff_on I I' n f sstates that the functionfisCⁿon the setscont_mdiff I I' n fstates that the functionfisCⁿ.cont_mdiff_on.compgives the invariance of theCⁿproperty under compositioncont_mdiff_iff_cont_diffstates that, for functions between vector spaces, manifold-smoothness is equivalent to usual smoothness.
We also give many basic properties of smooth functions between manifolds, following the API of smooth functions between vector spaces.
Implementation details #
Many properties follow for free from the corresponding properties of functions in vector spaces,
as being Cⁿ is a local property invariant under the smooth groupoid. We take advantage of the
general machinery developed in local_invariant_properties.lean to get these properties
automatically. For instance, the fact that being Cⁿ does not depend on the chart one considers
is given by lift_prop_within_at_indep_chart.
For this to work, the definition of cont_mdiff_within_at and friends has to
follow definitionally the setup of local invariant properties. Still, we recast the definition
in terms of extended charts in cont_mdiff_on_iff and cont_mdiff_iff.
Definition of smooth functions between manifolds #
def
cont_diff_within_at_prop
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(n : ℕ∞)
(f : H → H')
(s : set H)
(x : H) :
Prop
Property in the model space of a model with corners of being C^n within at set at a point,
when read in the model vector space. This property will be lifted to manifolds to define smooth
functions between manifolds.
theorem
cont_diff_within_at_prop_self_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{n : ℕ∞}
{f : E → H'}
{s : set E}
{x : E} :
cont_diff_within_at_prop (model_with_corners_self 𝕜 E) I' n f s x ↔ cont_diff_within_at 𝕜 n (⇑I' ∘ f) s x
theorem
cont_diff_within_at_prop_self
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : set E}
{x : E} :
cont_diff_within_at_prop (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s x ↔ cont_diff_within_at 𝕜 n f s x
theorem
cont_diff_within_at_prop_self_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : H → E'}
{s : set H}
{x : H} :
cont_diff_within_at_prop I (model_with_corners_self 𝕜 E') n f s x ↔ cont_diff_within_at 𝕜 n (f ∘ ⇑(I.symm)) (⇑(I.symm) ⁻¹' s ∩ set.range ⇑I) (⇑I x)
theorem
cont_diff_within_at_local_invariant_prop
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(n : ℕ∞) :
(cont_diff_groupoid ⊤ I).local_invariant_prop (cont_diff_groupoid ⊤ I') (cont_diff_within_at_prop I I' n)
Being Cⁿ in the model space is a local property, invariant under smooth maps. Therefore,
it will lift nicely to manifolds.
theorem
cont_diff_within_at_prop_mono_of_mem
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
(n : ℕ∞)
⦃s : set H⦄
⦃x : H⦄
⦃t : set H⦄
⦃f : H → H'⦄
(hts : s ∈ nhds_within x t)
(h : cont_diff_within_at_prop I I' n f s x) :
cont_diff_within_at_prop I I' n f t x
theorem
cont_diff_within_at_prop_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{n : ℕ∞}
(x : H) :
cont_diff_within_at_prop I I n id set.univ x
def
cont_mdiff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(n : ℕ∞)
(f : M → M')
(s : set M)
(x : M) :
Prop
A function is n times continuously differentiable within a set at a point in a manifold if
it is continuous and it is n times continuously differentiable in this set around this point, when
read in the preferred chart at this point.
Equations
- cont_mdiff_within_at I I' n f s x = charted_space.lift_prop_within_at (cont_diff_within_at_prop I I' n) f s x
@[reducible]
def
smooth_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : M → M')
(s : set M)
(x : M) :
Prop
Abbreviation for cont_mdiff_within_at I I' ⊤ f s x. See also documentation for smooth.
Equations
- smooth_within_at I I' f s x = cont_mdiff_within_at I I' ⊤ f s x
def
cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(n : ℕ∞)
(f : M → M')
(x : M) :
Prop
A function is n times continuously differentiable at a point in a manifold if
it is continuous and it is n times continuously differentiable around this point, when
read in the preferred chart at this point.
Equations
- cont_mdiff_at I I' n f x = cont_mdiff_within_at I I' n f set.univ x
theorem
cont_mdiff_at_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
{f : M → M'}
{x : M} :
cont_mdiff_at I I' n f x ↔ continuous_at f x ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (set.range ⇑I) (⇑(ext_chart_at I x) x)
@[reducible]
def
smooth_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : M → M')
(x : M) :
Prop
Abbreviation for cont_mdiff_at I I' ⊤ f x. See also documentation for smooth.
Equations
- smooth_at I I' f x = cont_mdiff_at I I' ⊤ f x
def
cont_mdiff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(n : ℕ∞)
(f : M → M')
(s : set M) :
Prop
A function is n times continuously differentiable in a set of a manifold if it is continuous
and, for any pair of points, it is n times continuously differentiable on this set in the charts
around these points.
Equations
- cont_mdiff_on I I' n f s = ∀ (x : M), x ∈ s → cont_mdiff_within_at I I' n f s x
@[reducible]
def
smooth_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : M → M')
(s : set M) :
Prop
Abbreviation for cont_mdiff_on I I' ⊤ f s. See also documentation for smooth.
Equations
- smooth_on I I' f s = cont_mdiff_on I I' ⊤ f s
def
cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(n : ℕ∞)
(f : M → M') :
Prop
A function is n times continuously differentiable in a manifold if it is continuous
and, for any pair of points, it is n times continuously differentiable in the charts
around these points.
Equations
- cont_mdiff I I' n f = ∀ (x : M), cont_mdiff_at I I' n f x
@[reducible]
def
smooth
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
(I' : model_with_corners 𝕜 E' H')
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : M → M') :
Prop
Abbreviation for cont_mdiff I I' ⊤ f.
Short note to work with these abbreviations: a lemma of the form cont_mdiff_foo.bar will
apply fine to an assumption smooth_foo using dot notation or normal notation.
If the consequence bar of the lemma involves cont_diff, it is still better to restate
the lemma replacing cont_diff with smooth both in the assumption and in the conclusion,
to make it possible to use smooth consistently.
This also applies to smooth_at, smooth_on and smooth_within_at.
Equations
- smooth I I' f = cont_mdiff I I' ⊤ f
Basic properties of smooth functions between manifolds #
theorem
cont_mdiff.smooth
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
(h : cont_mdiff I I' ⊤ f) :
smooth I I' f
theorem
smooth.cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
(h : smooth I I' f) :
cont_mdiff I I' ⊤ f
theorem
cont_mdiff_on.smooth_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
(h : cont_mdiff_on I I' ⊤ f s) :
smooth_on I I' f s
theorem
smooth_on.cont_mdiff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
(h : smooth_on I I' f s) :
cont_mdiff_on I I' ⊤ f s
theorem
cont_mdiff_at.smooth_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
(h : cont_mdiff_at I I' ⊤ f x) :
smooth_at I I' f x
theorem
smooth_at.cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
(h : smooth_at I I' f x) :
cont_mdiff_at I I' ⊤ f x
theorem
cont_mdiff_within_at.smooth_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
(h : cont_mdiff_within_at I I' ⊤ f s x) :
smooth_within_at I I' f s x
theorem
smooth_within_at.cont_mdiff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
(h : smooth_within_at I I' f s x) :
cont_mdiff_within_at I I' ⊤ f s x
theorem
cont_mdiff.cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
(h : cont_mdiff I I' n f) :
cont_mdiff_at I I' n f x
theorem
smooth.smooth_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
(h : smooth I I' f) :
smooth_at I I' f x
theorem
cont_mdiff_within_at_univ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
{n : ℕ∞} :
cont_mdiff_within_at I I' n f set.univ x ↔ cont_mdiff_at I I' n f x
theorem
smooth_within_at_univ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M} :
smooth_within_at I I' f set.univ x ↔ smooth_at I I' f x
theorem
cont_mdiff_on_univ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{n : ℕ∞} :
cont_mdiff_on I I' n f set.univ ↔ cont_mdiff I I' n f
theorem
smooth_on_univ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'} :
theorem
cont_mdiff_within_at_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞} :
cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x)
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart.
theorem
cont_mdiff_within_at_iff'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞} :
cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) ((ext_chart_at I x).target ∩ ⇑((ext_chart_at I x).symm) ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' (f x)).source)) (⇑(ext_chart_at I x) x)
One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart. This form states smoothness of f
written in such a way that the set is restricted to lie within the domain/codomain of the
corresponding charts.
Even though this expression is more complicated than the one in cont_mdiff_within_at_iff, it is
a smaller set, but their germs at ext_chart_at I x x are equal. It is sometimes useful to rewrite
using this in the goal.
theorem
cont_mdiff_within_at_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞} :
cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ cont_mdiff_within_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' (f x)) ∘ f) s x
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in the corresponding extended chart in the target.
theorem
smooth_within_at_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M} :
smooth_within_at I I' f s x ↔ continuous_within_at f s x ∧ cont_diff_within_at 𝕜 ⊤ (⇑(ext_chart_at I' (f x)) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x)
theorem
smooth_within_at_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M} :
smooth_within_at I I' f s x ↔ continuous_within_at f s x ∧ smooth_within_at I (model_with_corners_self 𝕜 E') (⇑(ext_chart_at I' (f x)) ∘ f) s x
theorem
cont_mdiff_at_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{n : ℕ∞}
{x : M} :
cont_mdiff_at I I' n f x ↔ continuous_at f x ∧ cont_mdiff_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' (f x)) ∘ f) x
theorem
smooth_at_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M} :
smooth_at I I' f x ↔ continuous_at f x ∧ smooth_at I (model_with_corners_self 𝕜 E') (⇑(ext_chart_at I' (f x)) ∘ f) x
theorem
cont_mdiff_within_at_iff_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{e : local_homeomorph M H}
{e' : local_homeomorph M' H'}
{f : M → M'}
{s : set M}
{n : ℕ∞}
{x : M}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(he' : e' ∈ smooth_manifold_with_corners.maximal_atlas I' M')
(hx : x ∈ e.to_local_equiv.source)
(hy : f x ∈ e'.to_local_equiv.source) :
theorem
cont_mdiff_within_at_iff_image
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{e : local_homeomorph M H}
{e' : local_homeomorph M' H'}
{f : M → M'}
{s : set M}
{n : ℕ∞}
{x : M}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(he' : e' ∈ smooth_manifold_with_corners.maximal_atlas I' M')
(hs : s ⊆ e.to_local_equiv.source)
(hx : x ∈ e.to_local_equiv.source)
(hy : f x ∈ e'.to_local_equiv.source) :
An alternative formulation of cont_mdiff_within_at_iff_of_mem_maximal_atlas
if the set if s lies in e.source.
theorem
cont_mdiff_within_at_iff_of_mem_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
{x' : M}
{y : M'}
(hx : x' ∈ (charted_space.chart_at H x).to_local_equiv.source)
(hy : f x' ∈ (charted_space.chart_at H' y).to_local_equiv.source) :
cont_mdiff_within_at I I' n f s x' ↔ continuous_within_at f s x' ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x')
One can reformulate smoothness within a set at a point as continuity within this set at this point, and smoothness in any chart containing that point.
theorem
cont_mdiff_within_at_iff_of_mem_source'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
{x' : M}
{y : M'}
(hx : x' ∈ (charted_space.chart_at H x).to_local_equiv.source)
(hy : f x' ∈ (charted_space.chart_at H' y).to_local_equiv.source) :
cont_mdiff_within_at I I' n f s x' ↔ continuous_within_at f s x' ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) ((ext_chart_at I x).target ∩ ⇑((ext_chart_at I x).symm) ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' y).source)) (⇑(ext_chart_at I x) x')
theorem
cont_mdiff_at_iff_of_mem_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
{x' : M}
{y : M'}
(hx : x' ∈ (charted_space.chart_at H x).to_local_equiv.source)
(hy : f x' ∈ (charted_space.chart_at H' y).to_local_equiv.source) :
cont_mdiff_at I I' n f x' ↔ continuous_at f x' ∧ cont_diff_within_at 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (set.range ⇑I) (⇑(ext_chart_at I x) x')
theorem
cont_mdiff_within_at_iff_target_of_mem_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{x : M}
{y : M'}
(hy : f x ∈ (charted_space.chart_at H' y).to_local_equiv.source) :
cont_mdiff_within_at I I' n f s x ↔ continuous_within_at f s x ∧ cont_mdiff_within_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' y) ∘ f) s x
theorem
cont_mdiff_at_iff_target_of_mem_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{n : ℕ∞}
{x : M}
{y : M'}
(hy : f x ∈ (charted_space.chart_at H' y).to_local_equiv.source) :
cont_mdiff_at I I' n f x ↔ continuous_at f x ∧ cont_mdiff_at I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' y) ∘ f) x
theorem
cont_mdiff_within_at_iff_source_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{e : local_homeomorph M H}
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(hx : x ∈ e.to_local_equiv.source) :
theorem
cont_mdiff_within_at_iff_source_of_mem_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
{x' : M}
(hx' : x' ∈ (charted_space.chart_at H x).to_local_equiv.source) :
cont_mdiff_within_at I I' n f s x' ↔ cont_mdiff_within_at (model_with_corners_self 𝕜 E) I' n (f ∘ ⇑((ext_chart_at I x).symm)) (⇑((ext_chart_at I x).symm) ⁻¹' s ∩ set.range ⇑I) (⇑(ext_chart_at I x) x')
theorem
cont_mdiff_at_iff_source_of_mem_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
{x' : M}
(hx' : x' ∈ (charted_space.chart_at H x).to_local_equiv.source) :
cont_mdiff_at I I' n f x' ↔ cont_mdiff_within_at (model_with_corners_self 𝕜 E) I' n (f ∘ ⇑((ext_chart_at I x).symm)) (set.range ⇑I) (⇑(ext_chart_at I x) x')
theorem
cont_mdiff_on_iff_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{e : local_homeomorph M H}
{e' : local_homeomorph M' H'}
{f : M → M'}
{s : set M}
{n : ℕ∞}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(he' : e' ∈ smooth_manifold_with_corners.maximal_atlas I' M')
(hs : s ⊆ e.to_local_equiv.source)
(h2s : set.maps_to f s e'.to_local_equiv.source) :
cont_mdiff_on I I' n f s ↔ continuous_on f s ∧ cont_diff_on 𝕜 n (⇑(e'.extend I') ∘ f ∘ ⇑((e.extend I).symm)) (⇑(e.extend I) '' s)
theorem
cont_mdiff_on_iff_of_subset_source
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{x : M}
{y : M'}
(hs : s ⊆ (charted_space.chart_at H x).to_local_equiv.source)
(h2s : set.maps_to f s (charted_space.chart_at H' y).to_local_equiv.source) :
cont_mdiff_on I I' n f s ↔ continuous_on f s ∧ cont_diff_on 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) (⇑(ext_chart_at I x) '' s)
If the set where you want f to be smooth lies entirely in a single chart, and f maps it
into a single chart, the smoothness of f on that set can be expressed by purely looking in
these charts.
Note: this lemma uses ext_chart_at I x '' s instead of (ext_chart_at I x).symm ⁻¹' s to ensure
that this set lies in (ext_chart_at I x).target.
theorem
cont_mdiff_on_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{n : ℕ∞} :
cont_mdiff_on I I' n f s ↔ continuous_on f s ∧ ∀ (x : M) (y : M'), cont_diff_on 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) ((ext_chart_at I x).target ∩ ⇑((ext_chart_at I x).symm) ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' y).source))
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.
theorem
cont_mdiff_on_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{n : ℕ∞} :
cont_mdiff_on I I' n f s ↔ continuous_on f s ∧ ∀ (y : M'), cont_mdiff_on I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' y) ∘ f) (s ∩ f ⁻¹' (ext_chart_at I' y).source)
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.
theorem
smooth_on_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M} :
smooth_on I I' f s ↔ continuous_on f s ∧ ∀ (x : M) (y : M'), cont_diff_on 𝕜 ⊤ (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) ((ext_chart_at I x).target ∩ ⇑((ext_chart_at I x).symm) ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' y).source))
theorem
smooth_on_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M} :
smooth_on I I' f s ↔ continuous_on f s ∧ ∀ (y : M'), smooth_on I (model_with_corners_self 𝕜 E') (⇑(ext_chart_at I' y) ∘ f) (s ∩ f ⁻¹' (ext_chart_at I' y).source)
theorem
cont_mdiff_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{n : ℕ∞} :
cont_mdiff I I' n f ↔ continuous f ∧ ∀ (x : M) (y : M'), cont_diff_on 𝕜 n (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) ((ext_chart_at I x).target ∩ ⇑((ext_chart_at I x).symm) ⁻¹' (f ⁻¹' (ext_chart_at I' y).source))
One can reformulate smoothness as continuity and smoothness in any extended chart.
theorem
cont_mdiff_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{n : ℕ∞} :
cont_mdiff I I' n f ↔ continuous f ∧ ∀ (y : M'), cont_mdiff_on I (model_with_corners_self 𝕜 E') n (⇑(ext_chart_at I' y) ∘ f) (f ⁻¹' (ext_chart_at I' y).source)
One can reformulate smoothness as continuity and smoothness in any extended chart in the target.
theorem
smooth_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'} :
smooth I I' f ↔ continuous f ∧ ∀ (x : M) (y : M'), cont_diff_on 𝕜 ⊤ (⇑(ext_chart_at I' y) ∘ f ∘ ⇑((ext_chart_at I x).symm)) ((ext_chart_at I x).target ∩ ⇑((ext_chart_at I x).symm) ⁻¹' (f ⁻¹' (ext_chart_at I' y).source))
theorem
smooth_iff_target
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'} :
smooth I I' f ↔ continuous f ∧ ∀ (y : M'), smooth_on I (model_with_corners_self 𝕜 E') (⇑(ext_chart_at I' y) ∘ f) (f ⁻¹' (ext_chart_at I' y).source)
Deducing smoothness from higher smoothness #
theorem
cont_mdiff_within_at.of_le
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{m n : ℕ∞}
(hf : cont_mdiff_within_at I I' n f s x)
(le : m ≤ n) :
cont_mdiff_within_at I I' m f s x
theorem
cont_mdiff_at.of_le
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
{m n : ℕ∞}
(hf : cont_mdiff_at I I' n f x)
(le : m ≤ n) :
cont_mdiff_at I I' m f x
theorem
cont_mdiff_on.of_le
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{m n : ℕ∞}
(hf : cont_mdiff_on I I' n f s)
(le : m ≤ n) :
cont_mdiff_on I I' m f s
theorem
cont_mdiff.of_le
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{m n : ℕ∞}
(hf : cont_mdiff I I' n f)
(le : m ≤ n) :
cont_mdiff I I' m f
Deducing smoothness from smoothness one step beyond #
theorem
cont_mdiff_within_at.of_succ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ}
(h : cont_mdiff_within_at I I' ↑(n.succ) f s x) :
cont_mdiff_within_at I I' ↑n f s x
theorem
cont_mdiff_at.of_succ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
{n : ℕ}
(h : cont_mdiff_at I I' ↑(n.succ) f x) :
cont_mdiff_at I I' ↑n f x
theorem
cont_mdiff_on.of_succ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{n : ℕ}
(h : cont_mdiff_on I I' ↑(n.succ) f s) :
cont_mdiff_on I I' ↑n f s
theorem
cont_mdiff.of_succ
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{n : ℕ}
(h : cont_mdiff I I' ↑(n.succ) f) :
cont_mdiff I I' ↑n f
Deducing continuity from smoothness #
theorem
cont_mdiff_within_at.continuous_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(hf : cont_mdiff_within_at I I' n f s x) :
continuous_within_at f s x
theorem
cont_mdiff_at.continuous_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
(hf : cont_mdiff_at I I' n f x) :
continuous_at f x
theorem
cont_mdiff_on.continuous_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{n : ℕ∞}
(hf : cont_mdiff_on I I' n f s) :
continuous_on f s
theorem
cont_mdiff.continuous
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{n : ℕ∞}
(hf : cont_mdiff I I' n f) :
C^∞ smoothness #
theorem
cont_mdiff_within_at_top
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M} :
smooth_within_at I I' f s x ↔ ∀ (n : ℕ), cont_mdiff_within_at I I' ↑n f s x
theorem
cont_mdiff_at_top
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M} :
theorem
cont_mdiff_on_top
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M} :
theorem
cont_mdiff_top
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'} :
theorem
cont_mdiff_within_at_iff_nat
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞} :
cont_mdiff_within_at I I' n f s x ↔ ∀ (m : ℕ), ↑m ≤ n → cont_mdiff_within_at I I' ↑m f s x
Restriction to a smaller set #
theorem
cont_mdiff_within_at.mono_of_mem
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s t : set M}
{x : M}
{n : ℕ∞}
(hf : cont_mdiff_within_at I I' n f s x)
(hts : s ∈ nhds_within x t) :
cont_mdiff_within_at I I' n f t x
theorem
cont_mdiff_within_at.mono
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s t : set M}
{x : M}
{n : ℕ∞}
(hf : cont_mdiff_within_at I I' n f s x)
(hts : t ⊆ s) :
cont_mdiff_within_at I I' n f t x
theorem
cont_mdiff_within_at_congr_nhds
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s t : set M}
{x : M}
{n : ℕ∞}
(hst : nhds_within x s = nhds_within x t) :
cont_mdiff_within_at I I' n f s x ↔ cont_mdiff_within_at I I' n f t x
theorem
cont_mdiff_at.cont_mdiff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(hf : cont_mdiff_at I I' n f x) :
cont_mdiff_within_at I I' n f s x
theorem
smooth_at.smooth_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
(hf : smooth_at I I' f x) :
smooth_within_at I I' f s x
theorem
cont_mdiff_on.mono
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s t : set M}
{n : ℕ∞}
(hf : cont_mdiff_on I I' n f s)
(hts : t ⊆ s) :
cont_mdiff_on I I' n f t
theorem
cont_mdiff.cont_mdiff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{n : ℕ∞}
(hf : cont_mdiff I I' n f) :
cont_mdiff_on I I' n f s
theorem
smooth.smooth_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
(hf : smooth I I' f) :
smooth_on I I' f s
theorem
cont_mdiff_within_at_inter'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s t : set M}
{x : M}
{n : ℕ∞}
(ht : t ∈ nhds_within x s) :
cont_mdiff_within_at I I' n f (s ∩ t) x ↔ cont_mdiff_within_at I I' n f s x
theorem
cont_mdiff_within_at_inter
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s t : set M}
{x : M}
{n : ℕ∞}
(ht : t ∈ nhds x) :
cont_mdiff_within_at I I' n f (s ∩ t) x ↔ cont_mdiff_within_at I I' n f s x
theorem
cont_mdiff_within_at.cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(h : cont_mdiff_within_at I I' n f s x)
(ht : s ∈ nhds x) :
cont_mdiff_at I I' n f x
theorem
smooth_within_at.smooth_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
(h : smooth_within_at I I' f s x)
(ht : s ∈ nhds x) :
smooth_at I I' f x
theorem
cont_mdiff_on.cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(h : cont_mdiff_on I I' n f s)
(hx : s ∈ nhds x) :
cont_mdiff_at I I' n f x
theorem
smooth_on.smooth_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
(h : smooth_on I I' f s)
(hx : s ∈ nhds x) :
smooth_at I I' f x
theorem
cont_mdiff_on_iff_source_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{e : local_homeomorph M H}
{f : M → M'}
{s : set M}
{n : ℕ∞}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(hs : s ⊆ e.to_local_equiv.source) :
cont_mdiff_on I I' n f s ↔ cont_mdiff_on (model_with_corners_self 𝕜 E) I' n (f ∘ ⇑((e.extend I).symm)) (⇑(e.extend I) '' s)
theorem
cont_mdiff_within_at_iff_cont_mdiff_on_nhds
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ} :
cont_mdiff_within_at I I' ↑n f s x ↔ ∃ (u : set M) (H_1 : u ∈ nhds_within x (has_insert.insert x s)), cont_mdiff_on I I' ↑n f u
A function is C^n within a set at a point, for n : ℕ, if and only if it is C^n on
a neighborhood of this point.
theorem
cont_mdiff_at_iff_cont_mdiff_on_nhds
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{x : M}
{n : ℕ} :
cont_mdiff_at I I' ↑n f x ↔ ∃ (u : set M) (H_1 : u ∈ nhds x), cont_mdiff_on I I' ↑n f u
A function is C^n at a point, for n : ℕ, if and only if it is C^n on
a neighborhood of this point.
theorem
cont_mdiff_at_iff_cont_mdiff_at_nhds
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{x : M}
{n : ℕ} :
cont_mdiff_at I I' ↑n f x ↔ ∀ᶠ (x' : M) in nhds x, cont_mdiff_at I I' ↑n f x'
Note: This does not hold for n = ∞. f being C^∞ at x means that for every n, f is
C^n on some neighborhood of x, but this neighborhood can depend on n.
Congruence lemmas #
theorem
cont_mdiff_within_at.congr
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(h : cont_mdiff_within_at I I' n f s x)
(h₁ : ∀ (y : M), y ∈ s → f₁ y = f y)
(hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x
theorem
cont_mdiff_within_at_congr
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(h₁ : ∀ (y : M), y ∈ s → f₁ y = f y)
(hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x ↔ cont_mdiff_within_at I I' n f s x
theorem
cont_mdiff_within_at.congr_of_eventually_eq
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(h : cont_mdiff_within_at I I' n f s x)
(h₁ : f₁ =ᶠ[nhds_within x s] f)
(hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x
theorem
filter.eventually_eq.cont_mdiff_within_at_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(h₁ : f₁ =ᶠ[nhds_within x s] f)
(hx : f₁ x = f x) :
cont_mdiff_within_at I I' n f₁ s x ↔ cont_mdiff_within_at I I' n f s x
theorem
cont_mdiff_at.congr_of_eventually_eq
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{x : M}
{n : ℕ∞}
(h : cont_mdiff_at I I' n f x)
(h₁ : f₁ =ᶠ[nhds x] f) :
cont_mdiff_at I I' n f₁ x
theorem
filter.eventually_eq.cont_mdiff_at_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{x : M}
{n : ℕ∞}
(h₁ : f₁ =ᶠ[nhds x] f) :
cont_mdiff_at I I' n f₁ x ↔ cont_mdiff_at I I' n f x
theorem
cont_mdiff_on.congr
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{s : set M}
{n : ℕ∞}
(h : cont_mdiff_on I I' n f s)
(h₁ : ∀ (y : M), y ∈ s → f₁ y = f y) :
cont_mdiff_on I I' n f₁ s
theorem
cont_mdiff_on_congr
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f f₁ : M → M'}
{s : set M}
{n : ℕ∞}
(h₁ : ∀ (y : M), y ∈ s → f₁ y = f y) :
cont_mdiff_on I I' n f₁ s ↔ cont_mdiff_on I I' n f s
Locality #
theorem
cont_mdiff_on_of_locally_cont_mdiff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{n : ℕ∞}
(h : ∀ (x : M), x ∈ s → (∃ (u : set M), is_open u ∧ x ∈ u ∧ cont_mdiff_on I I' n f (s ∩ u))) :
cont_mdiff_on I I' n f s
Being C^n is a local property.
theorem
cont_mdiff_of_locally_cont_mdiff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{n : ℕ∞}
(h : ∀ (x : M), ∃ (u : set M), is_open u ∧ x ∈ u ∧ cont_mdiff_on I I' n f u) :
cont_mdiff I I' n f
Smoothness of the composition of smooth functions between manifolds #
theorem
cont_mdiff_within_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{t : set M'}
{g : M' → M''}
(x : M)
(hg : cont_mdiff_within_at I' I'' n g t (f x))
(hf : cont_mdiff_within_at I I' n f s x)
(st : set.maps_to f s t) :
cont_mdiff_within_at I I'' n (g ∘ f) s x
The composition of C^n functions within domains at points is C^n.
theorem
cont_mdiff_within_at.comp_of_eq
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{t : set M'}
{g : M' → M''}
{x : M}
{y : M'}
(hg : cont_mdiff_within_at I' I'' n g t y)
(hf : cont_mdiff_within_at I I' n f s x)
(st : set.maps_to f s t)
(hx : f x = y) :
cont_mdiff_within_at I I'' n (g ∘ f) s x
theorem
smooth_within_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(x : M)
(hg : smooth_within_at I' I'' g t (f x))
(hf : smooth_within_at I I' f s x)
(st : set.maps_to f s t) :
smooth_within_at I I'' (g ∘ f) s x
The composition of C^∞ functions within domains at points is C^∞.
theorem
cont_mdiff_on.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{t : set M'}
{g : M' → M''}
(hg : cont_mdiff_on I' I'' n g t)
(hf : cont_mdiff_on I I' n f s)
(st : s ⊆ f ⁻¹' t) :
cont_mdiff_on I I'' n (g ∘ f) s
The composition of C^n functions on domains is C^n.
theorem
smooth_on.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(hg : smooth_on I' I'' g t)
(hf : smooth_on I I' f s)
(st : s ⊆ f ⁻¹' t) :
The composition of C^∞ functions on domains is C^∞.
theorem
cont_mdiff_on.comp'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{t : set M'}
{g : M' → M''}
(hg : cont_mdiff_on I' I'' n g t)
(hf : cont_mdiff_on I I' n f s) :
cont_mdiff_on I I'' n (g ∘ f) (s ∩ f ⁻¹' t)
The composition of C^n functions on domains is C^n.
theorem
smooth_on.comp'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(hg : smooth_on I' I'' g t)
(hf : smooth_on I I' f s) :
The composition of C^∞ functions is C^∞.
theorem
cont_mdiff.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{g : M' → M''}
(hg : cont_mdiff I' I'' n g)
(hf : cont_mdiff I I' n f) :
cont_mdiff I I'' n (g ∘ f)
The composition of C^n functions is C^n.
theorem
smooth.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{g : M' → M''}
(hg : smooth I' I'' g)
(hf : smooth I I' f) :
The composition of C^∞ functions is C^∞.
theorem
cont_mdiff_within_at.comp'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{t : set M'}
{g : M' → M''}
(x : M)
(hg : cont_mdiff_within_at I' I'' n g t (f x))
(hf : cont_mdiff_within_at I I' n f s x) :
cont_mdiff_within_at I I'' n (g ∘ f) (s ∩ f ⁻¹' t) x
The composition of C^n functions within domains at points is C^n.
theorem
smooth_within_at.comp'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{t : set M'}
{g : M' → M''}
(x : M)
(hg : smooth_within_at I' I'' g t (f x))
(hf : smooth_within_at I I' f s x) :
smooth_within_at I I'' (g ∘ f) (s ∩ f ⁻¹' t) x
The composition of C^∞ functions within domains at points is C^∞.
theorem
cont_mdiff_at.comp_cont_mdiff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{g : M' → M''}
(x : M)
(hg : cont_mdiff_at I' I'' n g (f x))
(hf : cont_mdiff_within_at I I' n f s x) :
cont_mdiff_within_at I I'' n (g ∘ f) s x
g ∘ f is C^n within s at x if g is C^n at f x and
f is C^n within s at x.
theorem
smooth_at.comp_smooth_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{s : set M}
{g : M' → M''}
(x : M)
(hg : smooth_at I' I'' g (f x))
(hf : smooth_within_at I I' f s x) :
smooth_within_at I I'' (g ∘ f) s x
g ∘ f is C^∞ within s at x if g is C^∞ at f x and
f is C^∞ within s at x.
theorem
cont_mdiff_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{g : M' → M''}
(x : M)
(hg : cont_mdiff_at I' I'' n g (f x))
(hf : cont_mdiff_at I I' n f x) :
cont_mdiff_at I I'' n (g ∘ f) x
The composition of C^n functions at points is C^n.
theorem
cont_mdiff_at.comp_of_eq
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{g : M' → M''}
{x : M}
{y : M'}
(hg : cont_mdiff_at I' I'' n g y)
(hf : cont_mdiff_at I I' n f x)
(hx : f x = y) :
cont_mdiff_at I I'' n (g ∘ f) x
theorem
smooth_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{g : M' → M''}
(x : M)
(hg : smooth_at I' I'' g (f x))
(hf : smooth_at I I' f x) :
The composition of C^∞ functions at points is C^∞.
theorem
cont_mdiff.comp_cont_mdiff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{n : ℕ∞}
{f : M → M'}
{g : M' → M''}
{s : set M}
(hg : cont_mdiff I' I'' n g)
(hf : cont_mdiff_on I I' n f s) :
cont_mdiff_on I I'' n (g ∘ f) s
theorem
smooth.comp_smooth_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{g : M' → M''}
{s : set M}
(hg : smooth I' I'' g)
(hf : smooth_on I I' f s) :
theorem
cont_mdiff_on.comp_cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{n : ℕ∞}
{t : set M'}
{g : M' → M''}
(hg : cont_mdiff_on I' I'' n g t)
(hf : cont_mdiff I I' n f)
(ht : ∀ (x : M), f x ∈ t) :
cont_mdiff I I'' n (g ∘ f)
theorem
smooth_on.comp_smooth
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{f : M → M'}
{t : set M'}
{g : M' → M''}
(hg : smooth_on I' I'' g t)
(hf : smooth I I' f)
(ht : ∀ (x : M), f x ∈ t) :
Atlas members are smooth #
theorem
cont_mdiff_model
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{n : ℕ∞} :
cont_mdiff I (model_with_corners_self 𝕜 E) n ⇑I
theorem
cont_mdiff_on_model_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{n : ℕ∞} :
cont_mdiff_on (model_with_corners_self 𝕜 E) I n ⇑(I.symm) (set.range ⇑I)
theorem
cont_mdiff_on_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{e : local_homeomorph M H}
{n : ℕ∞}
(h : e ∈ smooth_manifold_with_corners.maximal_atlas I M) :
cont_mdiff_on I I n ⇑e e.to_local_equiv.source
An atlas member is C^n for any n.
theorem
cont_mdiff_on_symm_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{e : local_homeomorph M H}
{n : ℕ∞}
(h : e ∈ smooth_manifold_with_corners.maximal_atlas I M) :
cont_mdiff_on I I n ⇑(e.symm) e.to_local_equiv.target
The inverse of an atlas member is C^n for any n.
theorem
cont_mdiff_at_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{e : local_homeomorph M H}
{x : M}
{n : ℕ∞}
(h : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(hx : x ∈ e.to_local_equiv.source) :
cont_mdiff_at I I n ⇑e x
theorem
cont_mdiff_at_symm_of_mem_maximal_atlas
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{e : local_homeomorph M H}
{n : ℕ∞}
{x : H}
(h : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(hx : x ∈ e.to_local_equiv.target) :
cont_mdiff_at I I n ⇑(e.symm) x
theorem
cont_mdiff_on_chart
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{x : M}
{n : ℕ∞} :
cont_mdiff_on I I n ⇑(charted_space.chart_at H x) (charted_space.chart_at H x).to_local_equiv.source
theorem
cont_mdiff_on_chart_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{x : M}
{n : ℕ∞} :
cont_mdiff_on I I n ⇑((charted_space.chart_at H x).symm) (charted_space.chart_at H x).to_local_equiv.target
theorem
cont_mdiff_at_extend
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{e : local_homeomorph M H}
{n : ℕ∞}
{x : M}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M)
(hx : x ∈ e.to_local_equiv.source) :
cont_mdiff_at I (model_with_corners_self 𝕜 E) n ⇑(e.extend I) x
theorem
cont_mdiff_at_ext_chart_at'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{x : M}
{n : ℕ∞}
{x' : M}
(h : x' ∈ (charted_space.chart_at H x).to_local_equiv.source) :
cont_mdiff_at I (model_with_corners_self 𝕜 E) n ⇑(ext_chart_at I x) x'
theorem
cont_mdiff_at_ext_chart_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{x : M}
{n : ℕ∞} :
cont_mdiff_at I (model_with_corners_self 𝕜 E) n ⇑(ext_chart_at I x) x
theorem
cont_mdiff_on_ext_chart_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{x : M}
{n : ℕ∞} :
cont_mdiff_on I (model_with_corners_self 𝕜 E) n ⇑(ext_chart_at I x) (charted_space.chart_at H x).to_local_equiv.source
theorem
cont_mdiff_on_extend_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{e : local_homeomorph M H}
{n : ℕ∞}
(he : e ∈ smooth_manifold_with_corners.maximal_atlas I M) :
cont_mdiff_on (model_with_corners_self 𝕜 E) I n ⇑((e.extend I).symm) (⇑I '' e.to_local_equiv.target)
theorem
cont_mdiff_on_ext_chart_at_symm
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{n : ℕ∞}
(x : M) :
cont_mdiff_on (model_with_corners_self 𝕜 E) I n ⇑((ext_chart_at I x).symm) (ext_chart_at I x).target
theorem
cont_mdiff_on_of_mem_cont_diff_groupoid
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{n : ℕ∞}
{e' : local_homeomorph H H}
(h : e' ∈ cont_diff_groupoid ⊤ I) :
cont_mdiff_on I I n ⇑e' e'.to_local_equiv.source
An element of cont_diff_groupoid ⊤ I is C^n for any n.
The identity is smooth #
theorem
cont_mdiff_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{n : ℕ∞} :
cont_mdiff I I n id
theorem
smooth_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M] :
theorem
cont_mdiff_on_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{n : ℕ∞} :
cont_mdiff_on I I n id s
theorem
smooth_on_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M} :
theorem
cont_mdiff_at_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M}
{n : ℕ∞} :
cont_mdiff_at I I n id x
theorem
smooth_at_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
theorem
cont_mdiff_within_at_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{x : M}
{n : ℕ∞} :
cont_mdiff_within_at I I n id s x
theorem
smooth_within_at_id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{x : M} :
smooth_within_at I I id s x
Constants are smooth #
theorem
cont_mdiff_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
{c : M'} :
cont_mdiff I I' n (λ (x : M), c)
theorem
cont_mdiff_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
[has_zero M'] :
cont_mdiff I I' n 0
theorem
cont_mdiff_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
[has_one M'] :
cont_mdiff I I' n 1
theorem
smooth_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{c : M'} :
smooth I I' (λ (x : M), c)
theorem
smooth_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[has_one M'] :
smooth I I' 1
theorem
smooth_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[has_zero M'] :
smooth I I' 0
theorem
cont_mdiff_on_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{n : ℕ∞}
{c : M'} :
cont_mdiff_on I I' n (λ (x : M), c) s
theorem
cont_mdiff_on_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{n : ℕ∞}
[has_zero M'] :
cont_mdiff_on I I' n 0 s
theorem
cont_mdiff_on_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{n : ℕ∞}
[has_one M'] :
cont_mdiff_on I I' n 1 s
theorem
smooth_on_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{c : M'} :
smooth_on I I' (λ (x : M), c) s
theorem
smooth_on_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
[has_one M'] :
smooth_on I I' 1 s
theorem
smooth_on_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
[has_zero M'] :
smooth_on I I' 0 s
theorem
cont_mdiff_at_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{x : M}
{n : ℕ∞}
{c : M'} :
cont_mdiff_at I I' n (λ (x : M), c) x
theorem
cont_mdiff_at_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{x : M}
{n : ℕ∞}
[has_zero M'] :
cont_mdiff_at I I' n 0 x
theorem
cont_mdiff_at_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{x : M}
{n : ℕ∞}
[has_one M'] :
cont_mdiff_at I I' n 1 x
theorem
smooth_at_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{x : M}
{c : M'} :
smooth_at I I' (λ (x : M), c) x
theorem
smooth_at_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{x : M}
[has_zero M'] :
smooth_at I I' 0 x
theorem
smooth_at_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{x : M}
[has_one M'] :
smooth_at I I' 1 x
theorem
cont_mdiff_within_at_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{x : M}
{n : ℕ∞}
{c : M'} :
cont_mdiff_within_at I I' n (λ (x : M), c) s x
theorem
cont_mdiff_within_at_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{x : M}
{n : ℕ∞}
[has_one M'] :
cont_mdiff_within_at I I' n 1 s x
theorem
cont_mdiff_within_at_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{x : M}
{n : ℕ∞}
[has_zero M'] :
cont_mdiff_within_at I I' n 0 s x
theorem
smooth_within_at_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{x : M}
{c : M'} :
smooth_within_at I I' (λ (x : M), c) s x
theorem
smooth_within_at_zero
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{x : M}
[has_zero M'] :
smooth_within_at I I' 0 s x
theorem
smooth_within_at_one
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{s : set M}
{x : M}
[has_one M'] :
smooth_within_at I I' 1 s x
theorem
cont_mdiff_of_support
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
{f : M → F}
(hf : ∀ (x : M), x ∈ tsupport f → cont_mdiff_at I (model_with_corners_self 𝕜 F) n f x) :
cont_mdiff I (model_with_corners_self 𝕜 F) n f
The inclusion map from one open set to another is smooth #
theorem
cont_mdiff_inclusion
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{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 : ℕ∞}
{U V : topological_space.opens M}
(h : U ≤ V) :
cont_mdiff I I n (set.inclusion h)
theorem
smooth_inclusion
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{U V : topological_space.opens M}
(h : U ≤ V) :
smooth I I (set.inclusion h)
Equivalence with the basic definition for functions between vector spaces #
theorem
cont_mdiff_within_at_iff_cont_diff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : set E}
{x : E} :
cont_mdiff_within_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s x ↔ cont_diff_within_at 𝕜 n f s x
theorem
cont_mdiff_within_at.cont_diff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : set E}
{x : E} :
cont_mdiff_within_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s x → cont_diff_within_at 𝕜 n f s x
Alias of the forward direction of cont_mdiff_within_at_iff_cont_diff_within_at.
theorem
cont_diff_within_at.cont_mdiff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : set E}
{x : E} :
cont_diff_within_at 𝕜 n f s x → cont_mdiff_within_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s x
Alias of the reverse direction of cont_mdiff_within_at_iff_cont_diff_within_at.
theorem
cont_mdiff_at_iff_cont_diff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{x : E} :
cont_mdiff_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f x ↔ cont_diff_at 𝕜 n f x
theorem
cont_diff_at.cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{x : E} :
cont_diff_at 𝕜 n f x → cont_mdiff_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f x
Alias of the reverse direction of cont_mdiff_at_iff_cont_diff_at.
theorem
cont_mdiff_at.cont_diff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{x : E} :
cont_mdiff_at (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f x → cont_diff_at 𝕜 n f x
Alias of the forward direction of cont_mdiff_at_iff_cont_diff_at.
theorem
cont_mdiff_on_iff_cont_diff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : set E} :
cont_mdiff_on (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s ↔ cont_diff_on 𝕜 n f s
theorem
cont_mdiff_on.cont_diff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : set E} :
cont_mdiff_on (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s → cont_diff_on 𝕜 n f s
Alias of the forward direction of cont_mdiff_on_iff_cont_diff_on.
theorem
cont_diff_on.cont_mdiff_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : set E} :
cont_diff_on 𝕜 n f s → cont_mdiff_on (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f s
Alias of the reverse direction of cont_mdiff_on_iff_cont_diff_on.
theorem
cont_mdiff_iff_cont_diff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'} :
cont_mdiff (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f ↔ cont_diff 𝕜 n f
theorem
cont_diff.cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'} :
cont_diff 𝕜 n f → cont_mdiff (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f
Alias of the reverse direction of cont_mdiff_iff_cont_diff.
theorem
cont_mdiff.cont_diff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{n : ℕ∞}
{f : E → E'} :
cont_mdiff (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') n f → cont_diff 𝕜 n f
Alias of the forward direction of cont_mdiff_iff_cont_diff.
theorem
cont_diff_within_at.comp_cont_mdiff_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{n : ℕ∞}
{g : F → F'}
{f : M → F}
{s : set M}
{t : set F}
{x : M}
(hg : cont_diff_within_at 𝕜 n g t (f x))
(hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 F) n f s x)
(h : s ⊆ f ⁻¹' t) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 F') n (g ∘ f) s x
theorem
cont_diff_at.comp_cont_mdiff_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{n : ℕ∞}
{g : F → F'}
{f : M → F}
{x : M}
(hg : cont_diff_at 𝕜 n g (f x))
(hf : cont_mdiff_at I (model_with_corners_self 𝕜 F) n f x) :
cont_mdiff_at I (model_with_corners_self 𝕜 F') n (g ∘ f) x
theorem
cont_diff.comp_cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{n : ℕ∞}
{g : F → F'}
{f : M → F}
(hg : cont_diff 𝕜 n g)
(hf : cont_mdiff I (model_with_corners_self 𝕜 F) n f) :
cont_mdiff I (model_with_corners_self 𝕜 F') n (g ∘ f)
Smoothness of standard maps associated to the product of manifolds #
theorem
cont_mdiff_within_at.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{s : set M}
{x : M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : cont_mdiff_within_at I I' n f s x)
(hg : cont_mdiff_within_at I J' n g s x) :
cont_mdiff_within_at I (I'.prod J') n (λ (x : M), (f x, g x)) s x
theorem
cont_mdiff_within_at.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{s : set M}
{x : M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 E') n f s x)
(hg : cont_mdiff_within_at I (model_with_corners_self 𝕜 F') n g s x) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x)) s x
theorem
cont_mdiff_at.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{x : M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : cont_mdiff_at I I' n f x)
(hg : cont_mdiff_at I J' n g x) :
cont_mdiff_at I (I'.prod J') n (λ (x : M), (f x, g x)) x
theorem
cont_mdiff_at.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{x : M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : cont_mdiff_at I (model_with_corners_self 𝕜 E') n f x)
(hg : cont_mdiff_at I (model_with_corners_self 𝕜 F') n g x) :
cont_mdiff_at I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x)) x
theorem
cont_mdiff_on.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{s : set M}
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : cont_mdiff_on I I' n f s)
(hg : cont_mdiff_on I J' n g s) :
cont_mdiff_on I (I'.prod J') n (λ (x : M), (f x, g x)) s
theorem
cont_mdiff_on.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{s : set M}
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : cont_mdiff_on I (model_with_corners_self 𝕜 E') n f s)
(hg : cont_mdiff_on I (model_with_corners_self 𝕜 F') n g s) :
cont_mdiff_on I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x)) s
theorem
cont_mdiff.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{n : ℕ∞}
{f : M → M'}
{g : M → N'}
(hf : cont_mdiff I I' n f)
(hg : cont_mdiff I J' n g) :
cont_mdiff I (I'.prod J') n (λ (x : M), (f x, g x))
theorem
cont_mdiff.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{n : ℕ∞}
{f : M → E'}
{g : M → F'}
(hf : cont_mdiff I (model_with_corners_self 𝕜 E') n f)
(hg : cont_mdiff I (model_with_corners_self 𝕜 F') n g) :
cont_mdiff I (model_with_corners_self 𝕜 (E' × F')) n (λ (x : M), (f x, g x))
theorem
smooth_within_at.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{s : set M}
{x : M}
{f : M → M'}
{g : M → N'}
(hf : smooth_within_at I I' f s x)
(hg : smooth_within_at I J' g s x) :
smooth_within_at I (I'.prod J') (λ (x : M), (f x, g x)) s x
theorem
smooth_within_at.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{s : set M}
{x : M}
{f : M → E'}
{g : M → F'}
(hf : smooth_within_at I (model_with_corners_self 𝕜 E') f s x)
(hg : smooth_within_at I (model_with_corners_self 𝕜 F') g s x) :
smooth_within_at I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x)) s x
theorem
smooth_at.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{x : M}
{f : M → M'}
{g : M → N'}
(hf : smooth_at I I' f x)
(hg : smooth_at I J' g x) :
theorem
smooth_at.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{x : M}
{f : M → E'}
{g : M → F'}
(hf : smooth_at I (model_with_corners_self 𝕜 E') f x)
(hg : smooth_at I (model_with_corners_self 𝕜 F') g x) :
smooth_at I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x)) x
theorem
smooth_on.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{s : set M}
{f : M → M'}
{g : M → N'}
(hf : smooth_on I I' f s)
(hg : smooth_on I J' g s) :
theorem
smooth_on.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{s : set M}
{f : M → E'}
{g : M → F'}
(hf : smooth_on I (model_with_corners_self 𝕜 E') f s)
(hg : smooth_on I (model_with_corners_self 𝕜 F') g s) :
smooth_on I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x)) s
theorem
smooth.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{g : M → N'}
(hf : smooth I I' f)
(hg : smooth I J' g) :
theorem
smooth.prod_mk_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{f : M → E'}
{g : M → F'}
(hf : smooth I (model_with_corners_self 𝕜 E') f)
(hg : smooth I (model_with_corners_self 𝕜 F') g) :
smooth I (model_with_corners_self 𝕜 (E' × F')) (λ (x : M), (f x, g x))
theorem
cont_mdiff_within_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{s : set (M × N)}
{p : M × N} :
cont_mdiff_within_at (I.prod J) I n prod.fst s p
theorem
cont_mdiff_within_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{f : N → M × M'}
{s : set N}
{x : N}
(hf : cont_mdiff_within_at J (I.prod I') n f s x) :
cont_mdiff_within_at J I n (λ (x : N), (f x).fst) s x
theorem
cont_mdiff_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{p : M × N} :
cont_mdiff_at (I.prod J) I n prod.fst p
theorem
cont_mdiff_on_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{s : set (M × N)} :
cont_mdiff_on (I.prod J) I n prod.fst s
theorem
cont_mdiff_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞} :
cont_mdiff (I.prod J) I n prod.fst
theorem
smooth_within_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{s : set (M × N)}
{p : M × N} :
smooth_within_at (I.prod J) I prod.fst s p
theorem
smooth_at_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{p : M × N} :
theorem
smooth_on_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{s : set (M × N)} :
theorem
smooth_fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N] :
theorem
cont_mdiff_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{f : N → M × M'}
{x : N}
(hf : cont_mdiff_at J (I.prod I') n f x) :
cont_mdiff_at J I n (λ (x : N), (f x).fst) x
theorem
cont_mdiff.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{f : N → M × M'}
(hf : cont_mdiff J (I.prod I') n f) :
cont_mdiff J I n (λ (x : N), (f x).fst)
theorem
smooth_at.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{f : N → M × M'}
{x : N}
(hf : smooth_at J (I.prod I') f x) :
theorem
smooth.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{f : N → M × M'}
(hf : smooth J (I.prod I') f) :
theorem
cont_mdiff_within_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{s : set (M × N)}
{p : M × N} :
cont_mdiff_within_at (I.prod J) J n prod.snd s p
theorem
cont_mdiff_within_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{f : N → M × M'}
{s : set N}
{x : N}
(hf : cont_mdiff_within_at J (I.prod I') n f s x) :
cont_mdiff_within_at J I' n (λ (x : N), (f x).snd) s x
theorem
cont_mdiff_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{p : M × N} :
cont_mdiff_at (I.prod J) J n prod.snd p
theorem
cont_mdiff_on_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{s : set (M × N)} :
cont_mdiff_on (I.prod J) J n prod.snd s
theorem
cont_mdiff_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞} :
cont_mdiff (I.prod J) J n prod.snd
theorem
smooth_within_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{s : set (M × N)}
{p : M × N} :
smooth_within_at (I.prod J) J prod.snd s p
theorem
smooth_at_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{p : M × N} :
theorem
smooth_on_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{s : set (M × N)} :
theorem
smooth_snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N] :
theorem
cont_mdiff_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{f : N → M × M'}
{x : N}
(hf : cont_mdiff_at J (I.prod I') n f x) :
cont_mdiff_at J I' n (λ (x : N), (f x).snd) x
theorem
cont_mdiff.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
{f : N → M × M'}
(hf : cont_mdiff J (I.prod I') n f) :
cont_mdiff J I' n (λ (x : N), (f x).snd)
theorem
smooth_at.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{f : N → M × M'}
{x : N}
(hf : smooth_at J (I.prod I') f x) :
theorem
smooth.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{f : N → M × M'}
(hf : smooth J (I.prod I') f) :
theorem
cont_mdiff_within_at_prod_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{n : ℕ∞}
(f : M → M' × N')
{s : set M}
{x : M} :
cont_mdiff_within_at I (I'.prod J') n f s x ↔ cont_mdiff_within_at I I' n (prod.fst ∘ f) s x ∧ cont_mdiff_within_at I J' n (prod.snd ∘ f) s x
theorem
cont_mdiff_at_prod_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{n : ℕ∞}
(f : M → M' × N')
{x : M} :
cont_mdiff_at I (I'.prod J') n f x ↔ cont_mdiff_at I I' n (prod.fst ∘ f) x ∧ cont_mdiff_at I J' n (prod.snd ∘ f) x
theorem
cont_mdiff_prod_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{n : ℕ∞}
(f : M → M' × N') :
cont_mdiff I (I'.prod J') n f ↔ cont_mdiff I I' n (prod.fst ∘ f) ∧ cont_mdiff I J' n (prod.snd ∘ f)
theorem
smooth_at_prod_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
(f : M → M' × N')
{x : M} :
theorem
smooth_prod_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
(f : M → M' × N') :
theorem
smooth_prod_assoc
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N] :
theorem
cont_mdiff_within_at.prod_map'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{g : N → N'}
{r : set N}
{p : M × N}
(hf : cont_mdiff_within_at I I' n f s p.fst)
(hg : cont_mdiff_within_at J J' n g r p.snd) :
cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s ×ˢ r) p
The product map of two C^n functions within a set at a point is C^n
within the product set at the product point.
theorem
cont_mdiff_within_at.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
{g : N → N'}
{r : set N}
{y : N}
(hf : cont_mdiff_within_at I I' n f s x)
(hg : cont_mdiff_within_at J J' n g r y) :
cont_mdiff_within_at (I.prod J) (I'.prod J') n (prod.map f g) (s ×ˢ r) (x, y)
theorem
cont_mdiff_at.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{x : M}
{n : ℕ∞}
{g : N → N'}
{y : N}
(hf : cont_mdiff_at I I' n f x)
(hg : cont_mdiff_at J J' n g y) :
cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) (x, y)
theorem
cont_mdiff_at.prod_map'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{n : ℕ∞}
{g : N → N'}
{p : M × N}
(hf : cont_mdiff_at I I' n f p.fst)
(hg : cont_mdiff_at J J' n g p.snd) :
cont_mdiff_at (I.prod J) (I'.prod J') n (prod.map f g) p
theorem
cont_mdiff_on.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{s : set M}
{n : ℕ∞}
{g : N → N'}
{r : set N}
(hf : cont_mdiff_on I I' n f s)
(hg : cont_mdiff_on J J' n g r) :
cont_mdiff_on (I.prod J) (I'.prod J') n (prod.map f g) (s ×ˢ r)
theorem
cont_mdiff.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{n : ℕ∞}
{g : N → N'}
(hf : cont_mdiff I I' n f)
(hg : cont_mdiff J J' n g) :
cont_mdiff (I.prod J) (I'.prod J') n (prod.map f g)
theorem
smooth_within_at.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{s : set M}
{x : M}
{g : N → N'}
{r : set N}
{y : N}
(hf : smooth_within_at I I' f s x)
(hg : smooth_within_at J J' g r y) :
smooth_within_at (I.prod J) (I'.prod J') (prod.map f g) (s ×ˢ r) (x, y)
theorem
smooth_at.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{x : M}
{g : N → N'}
{y : N}
(hf : smooth_at I I' f x)
(hg : smooth_at J J' g y) :
theorem
smooth_on.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{s : set M}
{g : N → N'}
{r : set N}
(hf : smooth_on I I' f s)
(hg : smooth_on J J' g r) :
theorem
smooth.prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{F' : Type u_14}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_15}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_16}
[topological_space N']
[charted_space G' N']
{f : M → M'}
{g : N → N'}
(hf : smooth I I' f)
(hg : smooth J J' g) :
Smoothness of functions with codomain Π i, F i #
We have no model_with_corners.pi yet, so we prove lemmas about functions f : M → Π i, F i and
use 𝓘(𝕜, Π i, F i) as the model space.
theorem
cont_mdiff_within_at_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{x : M}
{n : ℕ∞}
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
cont_mdiff_within_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ s x ↔ ∀ (i : ι), cont_mdiff_within_at I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i) s x
theorem
cont_mdiff_on_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{n : ℕ∞}
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
cont_mdiff_on I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ s ↔ ∀ (i : ι), cont_mdiff_on I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i) s
theorem
cont_mdiff_at_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M}
{n : ℕ∞}
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
cont_mdiff_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ x ↔ ∀ (i : ι), cont_mdiff_at I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i) x
theorem
cont_mdiff_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{n : ℕ∞}
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
cont_mdiff I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) n φ ↔ ∀ (i : ι), cont_mdiff I (model_with_corners_self 𝕜 (Fi i)) n (λ (x : M), φ x i)
theorem
smooth_within_at_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{x : M}
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
smooth_within_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ s x ↔ ∀ (i : ι), smooth_within_at I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i) s x
theorem
smooth_on_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
smooth_on I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ s ↔ ∀ (i : ι), smooth_on I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i) s
theorem
smooth_at_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M}
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
smooth_at I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ x ↔ ∀ (i : ι), smooth_at I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i) x
theorem
smooth_pi_space
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{ι : Type u_21}
[fintype ι]
{Fi : ι → Type u_22}
[Π (i : ι), normed_add_comm_group (Fi i)]
[Π (i : ι), normed_space 𝕜 (Fi i)]
{φ : M → Π (i : ι), Fi i} :
smooth I (model_with_corners_self 𝕜 (Π (i : ι), Fi i)) φ ↔ ∀ (i : ι), smooth I (model_with_corners_self 𝕜 (Fi i)) (λ (x : M), φ x i)
Linear maps between normed spaces are smooth #
theorem
continuous_linear_map.cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{n : ℕ∞}
(L : E →L[𝕜] F) :
cont_mdiff (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 F) n ⇑L
theorem
cont_mdiff_within_at.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₁)}
{s : set M}
{x : M}
(hg : cont_mdiff_within_at I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g s x)
(hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₁)) n f s x) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₃)) n (λ (x : M), (g x).comp (f x)) s x
theorem
cont_mdiff_at.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₁)}
{x : M}
(hg : cont_mdiff_at I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g x)
(hf : cont_mdiff_at I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₁)) n f x) :
cont_mdiff_at I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₃)) n (λ (x : M), (g x).comp (f x)) x
theorem
cont_mdiff_on.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₁)}
{s : set M}
(hg : cont_mdiff_on I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g s)
(hf : cont_mdiff_on I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₁)) n f s) :
cont_mdiff_on I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₃)) n (λ (x : M), (g x).comp (f x)) s
theorem
cont_mdiff.clm_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₁)}
(hg : cont_mdiff I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g)
(hf : cont_mdiff I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₁)) n f) :
cont_mdiff I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₃)) n (λ (x : M), (g x).comp (f x))
theorem
cont_mdiff_within_at.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{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_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₂)}
{f : M → F₁}
{s : set M}
{x : M}
(hg : cont_mdiff_within_at I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₂)) n g s x)
(hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 F₁) n f s x) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 F₂) n (λ (x : M), ⇑(g x) (f x)) s x
theorem
cont_mdiff_at.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{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_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₂)}
{f : M → F₁}
{x : M}
(hg : cont_mdiff_at I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₂)) n g x)
(hf : cont_mdiff_at I (model_with_corners_self 𝕜 F₁) n f x) :
cont_mdiff_at I (model_with_corners_self 𝕜 F₂) n (λ (x : M), ⇑(g x) (f x)) x
theorem
cont_mdiff_on.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{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_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₂)}
{f : M → F₁}
{s : set M}
(hg : cont_mdiff_on I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₂)) n g s)
(hf : cont_mdiff_on I (model_with_corners_self 𝕜 F₁) n f s) :
cont_mdiff_on I (model_with_corners_self 𝕜 F₂) n (λ (x : M), ⇑(g x) (f x)) s
theorem
cont_mdiff.clm_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{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_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₂)}
{f : M → F₁}
(hg : cont_mdiff I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₂)) n g)
(hf : cont_mdiff I (model_with_corners_self 𝕜 F₁) n f) :
cont_mdiff I (model_with_corners_self 𝕜 F₂) n (λ (x : M), ⇑(g x) (f x))
theorem
cont_mdiff_within_at.clm_prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{F₄ : Type u_20}
[normed_add_comm_group F₄]
[normed_space 𝕜 F₄]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₄)}
{s : set M}
{x : M}
(hg : cont_mdiff_within_at I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g s x)
(hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₄)) n f s x) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (λ (x : M), (g x).prod_map (f x)) s x
theorem
cont_mdiff_at.clm_prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{F₄ : Type u_20}
[normed_add_comm_group F₄]
[normed_space 𝕜 F₄]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₄)}
{x : M}
(hg : cont_mdiff_at I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g x)
(hf : cont_mdiff_at I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₄)) n f x) :
cont_mdiff_at I (model_with_corners_self 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (λ (x : M), (g x).prod_map (f x)) x
theorem
cont_mdiff_on.clm_prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{F₄ : Type u_20}
[normed_add_comm_group F₄]
[normed_space 𝕜 F₄]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₄)}
{s : set M}
(hg : cont_mdiff_on I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g s)
(hf : cont_mdiff_on I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₄)) n f s) :
cont_mdiff_on I (model_with_corners_self 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (λ (x : M), (g x).prod_map (f x)) s
theorem
cont_mdiff.clm_prod_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{F₁ : Type u_17}
[normed_add_comm_group F₁]
[normed_space 𝕜 F₁]
{F₂ : Type u_18}
[normed_add_comm_group F₂]
[normed_space 𝕜 F₂]
{F₃ : Type u_19}
[normed_add_comm_group F₃]
[normed_space 𝕜 F₃]
{F₄ : Type u_20}
[normed_add_comm_group F₄]
[normed_space 𝕜 F₄]
{n : ℕ∞}
{g : M → (F₁ →L[𝕜] F₃)}
{f : M → (F₂ →L[𝕜] F₄)}
(hg : cont_mdiff I (model_with_corners_self 𝕜 (F₁ →L[𝕜] F₃)) n g)
(hf : cont_mdiff I (model_with_corners_self 𝕜 (F₂ →L[𝕜] F₄)) n f) :
cont_mdiff I (model_with_corners_self 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (λ (x : M), (g x).prod_map (f x))
Smoothness of standard operations #
theorem
smooth_smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V] :
smooth ((model_with_corners_self 𝕜 𝕜).prod (model_with_corners_self 𝕜 V)) (model_with_corners_self 𝕜 V) (λ (p : 𝕜 × V), p.fst • p.snd)
On any vector space, multiplication by a scalar is a smooth operation.
theorem
cont_mdiff_within_at.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{x : M}
{n : ℕ∞}
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : cont_mdiff_within_at I (model_with_corners_self 𝕜 𝕜) n f s x)
(hg : cont_mdiff_within_at I (model_with_corners_self 𝕜 V) n g s x) :
cont_mdiff_within_at I (model_with_corners_self 𝕜 V) n (λ (p : M), f p • g p) s x
theorem
cont_mdiff_at.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M}
{n : ℕ∞}
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : cont_mdiff_at I (model_with_corners_self 𝕜 𝕜) n f x)
(hg : cont_mdiff_at I (model_with_corners_self 𝕜 V) n g x) :
cont_mdiff_at I (model_with_corners_self 𝕜 V) n (λ (p : M), f p • g p) x
theorem
cont_mdiff_on.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{n : ℕ∞}
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : cont_mdiff_on I (model_with_corners_self 𝕜 𝕜) n f s)
(hg : cont_mdiff_on I (model_with_corners_self 𝕜 V) n g s) :
cont_mdiff_on I (model_with_corners_self 𝕜 V) n (λ (p : M), f p • g p) s
theorem
cont_mdiff.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{n : ℕ∞}
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : cont_mdiff I (model_with_corners_self 𝕜 𝕜) n f)
(hg : cont_mdiff I (model_with_corners_self 𝕜 V) n g) :
cont_mdiff I (model_with_corners_self 𝕜 V) n (λ (p : M), f p • g p)
theorem
smooth_within_at.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{x : M}
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : smooth_within_at I (model_with_corners_self 𝕜 𝕜) f s x)
(hg : smooth_within_at I (model_with_corners_self 𝕜 V) g s x) :
smooth_within_at I (model_with_corners_self 𝕜 V) (λ (p : M), f p • g p) s x
theorem
smooth_at.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M}
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : smooth_at I (model_with_corners_self 𝕜 𝕜) f x)
(hg : smooth_at I (model_with_corners_self 𝕜 V) g x) :
smooth_at I (model_with_corners_self 𝕜 V) (λ (p : M), f p • g p) x
theorem
smooth_on.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{s : set M}
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : smooth_on I (model_with_corners_self 𝕜 𝕜) f s)
(hg : smooth_on I (model_with_corners_self 𝕜 V) g s) :
smooth_on I (model_with_corners_self 𝕜 V) (λ (p : M), f p • g p) s
theorem
smooth.smul
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{V : Type u_21}
[normed_add_comm_group V]
[normed_space 𝕜 V]
{f : M → 𝕜}
{g : M → V}
(hf : smooth I (model_with_corners_self 𝕜 𝕜) f)
(hg : smooth I (model_with_corners_self 𝕜 V) g) :
smooth I (model_with_corners_self 𝕜 V) (λ (p : M), f p • g p)
Smoothness of (local) structomorphisms #
theorem
is_local_structomorph_on_cont_diff_groupoid_iff_aux
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H M']
[IsM' : smooth_manifold_with_corners I M']
{f : local_homeomorph M M'}
(hf : charted_space.lift_prop_on (cont_diff_groupoid ⊤ I).is_local_structomorph_within_at ⇑f f.to_local_equiv.source) :
smooth_on I I ⇑f f.to_local_equiv.source
theorem
is_local_structomorph_on_cont_diff_groupoid_iff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{M' : Type u_7}
[topological_space M']
[charted_space H M']
[IsM' : smooth_manifold_with_corners I M']
(f : local_homeomorph M M') :
Let M and M' be smooth manifolds with the same model-with-corners, I. Then f : M → M'
is a local structomorphism for I, if and only if it is manifold-smooth on the domain of definition
in both directions.