Smooth functions between smooth manifolds #
We define Cⁿ functions between smooth manifolds, as functions which are Cⁿ in charts, and prove
basic properties of these notions.
Main definitions and statements #
Let M and M' be two smooth manifolds, with respect to model with corners I and I'. Let
f : M → M'.
ContMDiffWithinAt I I' n f s xstates that the functionfisCⁿwithin the setsaround the pointx.ContMDiffAt I I' n f xstates that the functionfisCⁿaroundx.ContMDiffOn I I' n f sstates that the functionfisCⁿon the setsContMDiff I I' n fstates that the functionfisCⁿ.
We also give some basic properties of smooth functions between manifolds, following the API of
smooth functions between vector spaces.
See Basic.lean for further basic properties of smooth functions between smooth manifolds,
NormedSpace.lean for the equivalence of manifold-smoothness to usual smoothness,
Product.lean for smoothness results related to the product of manifolds and
Atlas.lean for smoothness of atlas members and local structomorphisms.
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 LocalInvariantProperties.lean to get these properties
automatically. For instance, the fact that being Cⁿ does not depend on the chart one considers
is given by liftPropWithinAt_indep_chart.
For this to work, the definition of ContMDiffWithinAt and friends has to
follow definitionally the setup of local invariant properties. Still, we recast the definition
in terms of extended charts in contMDiffOn_iff and contMDiff_iff.
Definition of smooth functions between manifolds #
def
ContDiffWithinAtProp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
(n : ℕ∞)
(f : H → H')
(s : Set H)
(x : H)
:
Property in the model space of a model with corners of being C^n within at set at a point,
when read in the model vector space. This property will be lifted to manifolds to define smooth
functions between manifolds.
Equations
- ContDiffWithinAtProp I I' n f s x = ContDiffWithinAt 𝕜 (↑n) (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
Instances For
theorem
contDiffWithinAtProp_self_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{n : ℕ∞}
{f : E → H'}
{s : Set E}
{x : E}
:
ContDiffWithinAtProp (modelWithCornersSelf 𝕜 E) I' n f s x ↔ ContDiffWithinAt 𝕜 (↑n) (↑I' ∘ f) s x
theorem
contDiffWithinAtProp_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{n : ℕ∞}
{f : E → E'}
{s : Set E}
{x : E}
:
ContDiffWithinAtProp (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x ↔ ContDiffWithinAt 𝕜 (↑n) f s x
theorem
contDiffWithinAtProp_self_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{n : ℕ∞}
{f : H → E'}
{s : Set H}
{x : H}
:
ContDiffWithinAtProp I (modelWithCornersSelf 𝕜 E') n f s x ↔ ContDiffWithinAt 𝕜 (↑n) (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
theorem
contDiffWithinAt_localInvariantProp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(n : ℕ∞)
:
(contDiffGroupoid (↑⊤) I).LocalInvariantProp (contDiffGroupoid (↑⊤) I') (ContDiffWithinAtProp 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
contDiffWithinAtProp_mono_of_mem_nhdsWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(n : ℕ∞)
⦃s : Set H⦄
⦃x : H⦄
⦃t : Set H⦄
⦃f : H → H'⦄
(hts : s ∈ nhdsWithin x t)
(h : ContDiffWithinAtProp I I' n f s x)
:
ContDiffWithinAtProp I I' n f t x
@[deprecated contDiffWithinAtProp_mono_of_mem_nhdsWithin]
theorem
contDiffWithinAtProp_mono_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
(n : ℕ∞)
⦃s : Set H⦄
⦃x : H⦄
⦃t : Set H⦄
⦃f : H → H'⦄
(hts : s ∈ nhdsWithin x t)
(h : ContDiffWithinAtProp I I' n f s x)
:
ContDiffWithinAtProp I I' n f t x
theorem
contDiffWithinAtProp_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{n : ℕ∞}
(x : H)
:
ContDiffWithinAtProp I I n id Set.univ x
def
ContMDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
(s : Set M)
(x : M)
:
A function is n times continuously differentiable within a set at a point in a manifold if
it is continuous and it is n times continuously differentiable in this set around this point, when
read in the preferred chart at this point.
Equations
- ContMDiffWithinAt I I' n f s x = ChartedSpace.LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
Instances For
@[deprecated ContMDiffWithinAt]
def
SmoothWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
(s : Set M)
(x : M)
:
Alias of ContMDiffWithinAt.
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
Instances For
def
ContMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
(x : M)
:
A function is n times continuously differentiable at a point in a manifold if
it is continuous and it is n times continuously differentiable around this point, when
read in the preferred chart at this point.
Equations
- ContMDiffAt I I' n f x = ContMDiffWithinAt I I' n f Set.univ x
Instances For
theorem
contMDiffAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{n : ℕ∞}
{f : M → M'}
{x : M}
:
ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContDiffWithinAt 𝕜 (↑n) (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x)
@[deprecated ContMDiffAt]
def
SmoothAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
(x : M)
:
Alias of ContMDiffAt.
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
Instances For
def
ContMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
(s : Set M)
:
A function is n times continuously differentiable in a set of a manifold if it is continuous
and, for any pair of points, it is n times continuously differentiable on this set in the charts
around these points.
Equations
- ContMDiffOn I I' n f s = ∀ x ∈ s, ContMDiffWithinAt I I' n f s x
Instances For
@[deprecated ContMDiffOn]
def
SmoothOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
(s : Set M)
:
Alias of ContMDiffOn.
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
Instances For
def
ContMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
:
A function is n times continuously differentiable in a manifold if it is continuous
and, for any pair of points, it is n times continuously differentiable in the charts
around these points.
Equations
- ContMDiff I I' n f = ∀ (x : M), ContMDiffAt I I' n f x
Instances For
@[deprecated ContMDiff]
def
Smooth
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(n : ℕ∞)
(f : M → M')
:
Alias of ContMDiff.
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.
Instances For
Deducing smoothness from higher smoothness #
theorem
ContMDiffWithinAt.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{m n : ℕ∞}
(hf : ContMDiffWithinAt I I' n f s x)
(le : m ≤ n)
:
ContMDiffWithinAt I I' m f s x
theorem
ContMDiffAt.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{m n : ℕ∞}
(hf : ContMDiffAt I I' n f x)
(le : m ≤ n)
:
ContMDiffAt I I' m f x
theorem
ContMDiffOn.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{m n : ℕ∞}
(hf : ContMDiffOn I I' n f s)
(le : m ≤ n)
:
ContMDiffOn I I' m f s
theorem
ContMDiff.of_le
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{m n : ℕ∞}
(hf : ContMDiff I I' n f)
(le : m ≤ n)
:
ContMDiff I I' m f
Basic properties of smooth functions between manifolds #
@[deprecated ContMDiff.of_le]
theorem
ContMDiff.smooth
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{m n : ℕ∞}
(hf : ContMDiff I I' n f)
(le : m ≤ n)
:
ContMDiff I I' m f
Alias of ContMDiff.of_le.
@[deprecated ContMDiff.of_le]
theorem
Smooth.contMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{m n : ℕ∞}
(hf : ContMDiff I I' n f)
(le : m ≤ n)
:
ContMDiff I I' m f
Alias of ContMDiff.of_le.
@[deprecated ContMDiffOn.of_le]
theorem
ContMDiffOn.smoothOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{m n : ℕ∞}
(hf : ContMDiffOn I I' n f s)
(le : m ≤ n)
:
ContMDiffOn I I' m f s
Alias of ContMDiffOn.of_le.
@[deprecated ContMDiffOn.of_le]
theorem
SmoothOn.contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{m n : ℕ∞}
(hf : ContMDiffOn I I' n f s)
(le : m ≤ n)
:
ContMDiffOn I I' m f s
Alias of ContMDiffOn.of_le.
@[deprecated ContMDiffAt.of_le]
theorem
ContMDiffAt.smoothAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{m n : ℕ∞}
(hf : ContMDiffAt I I' n f x)
(le : m ≤ n)
:
ContMDiffAt I I' m f x
Alias of ContMDiffAt.of_le.
@[deprecated ContMDiffOn.of_le]
theorem
SmoothAt.contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{m n : ℕ∞}
(hf : ContMDiffOn I I' n f s)
(le : m ≤ n)
:
ContMDiffOn I I' m f s
Alias of ContMDiffOn.of_le.
@[deprecated ContMDiffWithinAt.of_le]
theorem
ContMDiffWithinAt.smoothWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{m n : ℕ∞}
(hf : ContMDiffWithinAt I I' n f s x)
(le : m ≤ n)
:
ContMDiffWithinAt I I' m f s x
Alias of ContMDiffWithinAt.of_le.
@[deprecated ContMDiffWithinAt.of_le]
theorem
SmoothWithinAt.contMDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{m n : ℕ∞}
(hf : ContMDiffWithinAt I I' n f s x)
(le : m ≤ n)
:
ContMDiffWithinAt I I' m f s x
Alias of ContMDiffWithinAt.of_le.
theorem
ContMDiff.contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
(h : ContMDiff I I' n f)
:
ContMDiffAt I I' n f x
@[deprecated ContMDiff.contMDiffAt]
theorem
Smooth.smoothAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
(h : ContMDiff I I' n f)
:
ContMDiffAt I I' n f x
Alias of ContMDiff.contMDiffAt.
theorem
contMDiffWithinAt_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f Set.univ x ↔ ContMDiffAt I I' n f x
@[deprecated contMDiffWithinAt_univ]
theorem
smoothWithinAt_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f Set.univ x ↔ ContMDiffAt I I' n f x
Alias of contMDiffWithinAt_univ.
theorem
contMDiffOn_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
:
ContMDiffOn I I' n f Set.univ ↔ ContMDiff I I' n f
@[deprecated contMDiffOn_univ]
theorem
smoothOn_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
:
ContMDiffOn I I' n f Set.univ ↔ ContMDiff I I' n f
Alias of contMDiffOn_univ.
theorem
contMDiffWithinAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 (↑n) (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt 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
contMDiffWithinAt_iff'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 (↑n) (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
(↑(extChartAt 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 contMDiffWithinAt_iff, it is
a smaller set, but their germs at extChartAt I x x are equal. It is sometimes useful to rewrite
using this in the goal.
theorem
contMDiffWithinAt_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt 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.
@[deprecated contMDiffWithinAt_iff]
theorem
smoothWithinAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 (↑n) (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
Alias of contMDiffWithinAt_iff.
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.
@[deprecated contMDiffWithinAt_iff_target]
theorem
smoothWithinAt_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' (f x)) ∘ f) s x
Alias of contMDiffWithinAt_iff_target.
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
contMDiffAt_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
{x : M}
:
ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' (f x)) ∘ f) x
@[deprecated contMDiffAt_iff_target]
theorem
smoothAt_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
{x : M}
:
ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' (f x)) ∘ f) x
Alias of contMDiffAt_iff_target.
theorem
contMDiffWithinAt_iff_source_of_mem_maximalAtlas
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : PartialHomeomorph M H}
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
(he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M)
(hx : x ∈ e.source)
:
ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ Set.range ↑I)
(↑(e.extend I) x)
theorem
contMDiffWithinAt_iff_source_of_mem_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
{x' : M}
(hx' : x' ∈ (chartAt H x).source)
:
ContMDiffWithinAt I I' n f s x' ↔ ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(extChartAt I x).symm)
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x')
theorem
contMDiffAt_iff_source_of_mem_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
{x' : M}
(hx' : x' ∈ (chartAt H x).source)
:
ContMDiffAt I I' n f x' ↔ ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x')
theorem
contMDiffWithinAt_iff_target_of_mem_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I' M']
{x : M}
{y : M'}
(hy : f x ∈ (chartAt H' y).source)
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) s x
theorem
contMDiffAt_iff_target_of_mem_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
[SmoothManifoldWithCorners I' M']
{x : M}
{y : M'}
(hy : f x ∈ (chartAt H' y).source)
:
ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) x
theorem
contMDiffWithinAt_iff_of_mem_maximalAtlas
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : PartialHomeomorph M H}
{e' : PartialHomeomorph M' H'}
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M)
(he' : e' ∈ SmoothManifoldWithCorners.maximalAtlas I' M')
(hx : x ∈ e.source)
(hy : f x ∈ e'.source)
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 (↑n) (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ Set.range ↑I)
(↑(e.extend I) x)
theorem
contMDiffWithinAt_iff_image
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : PartialHomeomorph M H}
{e' : PartialHomeomorph M' H'}
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M)
(he' : e' ∈ SmoothManifoldWithCorners.maximalAtlas I' M')
(hs : s ⊆ e.source)
(hx : x ∈ e.source)
(hy : f x ∈ e'.source)
:
ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 (↑n) (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)
An alternative formulation of contMDiffWithinAt_iff_of_mem_maximalAtlas
if the set if s lies in e.source.
theorem
contMDiffWithinAt_iff_of_mem_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x' : M}
{y : M'}
(hx : x' ∈ (chartAt H x).source)
(hy : f x' ∈ (chartAt H' y).source)
:
ContMDiffWithinAt I I' n f s x' ↔ ContinuousWithinAt f s x' ∧ ContDiffWithinAt 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt 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
contMDiffWithinAt_iff_of_mem_source'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x' : M}
{y : M'}
(hx : x' ∈ (chartAt H x).source)
(hy : f x' ∈ (chartAt H' y).source)
:
ContMDiffWithinAt I I' n f s x' ↔ ContinuousWithinAt f s x' ∧ ContDiffWithinAt 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) (↑(extChartAt I x) x')
theorem
contMDiffAt_iff_of_mem_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x' : M}
{y : M'}
(hx : x' ∈ (chartAt H x).source)
(hy : f x' ∈ (chartAt H' y).source)
:
ContMDiffAt I I' n f x' ↔ ContinuousAt f x' ∧ ContDiffWithinAt 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x')
theorem
contMDiffOn_iff_of_mem_maximalAtlas
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : PartialHomeomorph M H}
{e' : PartialHomeomorph M' H'}
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M)
(he' : e' ∈ SmoothManifoldWithCorners.maximalAtlas I' M')
(hs : s ⊆ e.source)
(h2s : Set.MapsTo f s e'.source)
:
ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ContDiffOn 𝕜 (↑n) (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
theorem
contMDiffOn_iff_of_mem_maximalAtlas'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : PartialHomeomorph M H}
{e' : PartialHomeomorph M' H'}
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M)
(he' : e' ∈ SmoothManifoldWithCorners.maximalAtlas I' M')
(hs : s ⊆ e.source)
(h2s : Set.MapsTo f s e'.source)
:
ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 (↑n) (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
theorem
contMDiffOn_iff_of_subset_source
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
{y : M'}
(hs : s ⊆ (chartAt H x).source)
(h2s : Set.MapsTo f s (chartAt H' y).source)
:
ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ContDiffOn 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt 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 extChartAt I x '' s instead of (extChartAt I x).symm ⁻¹' s to ensure
that this set lies in (extChartAt I x).target.
theorem
contMDiffOn_iff_of_subset_source'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
{y : M'}
(hs : s ⊆ (extChartAt I x).source)
(h2s : Set.MapsTo f s (extChartAt I' y).source)
:
ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt 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 extChartAt I x '' s instead of (extChartAt I x).symm ⁻¹' s to ensure
that this set lies in (extChartAt I x).target.
theorem
contMDiffOn_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ∀ (x : M) (y : M'),
ContDiffOn 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.
theorem
contMDiffOn_zero_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiffOn I I' 0 f s ↔ ContinuousOn f s
zero-smoothness on a set is equivalent to continuity on this set.
theorem
contMDiffOn_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ∀ (y : M'),
ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.
@[deprecated contMDiffOn_iff]
theorem
smoothOn_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ∀ (x : M) (y : M'),
ContDiffOn 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
Alias of contMDiffOn_iff.
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart.
@[deprecated contMDiffOn_iff_target]
theorem
smoothOn_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ∀ (y : M'),
ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)
Alias of contMDiffOn_iff_target.
One can reformulate smoothness on a set as continuity on this set, and smoothness in any extended chart in the target.
theorem
contMDiff_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiff I I' n f ↔ Continuous f ∧ ∀ (x : M) (y : M'),
ContDiffOn 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))
One can reformulate smoothness as continuity and smoothness in any extended chart.
theorem
contMDiff_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiff I I' n f ↔ Continuous f ∧ ∀ (y : M'), ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)
One can reformulate smoothness as continuity and smoothness in any extended chart in the target.
@[deprecated contMDiff_iff]
theorem
smooth_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiff I I' n f ↔ Continuous f ∧ ∀ (x : M) (y : M'),
ContDiffOn 𝕜 (↑n) (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))
Alias of contMDiff_iff.
One can reformulate smoothness as continuity and smoothness in any extended chart.
@[deprecated contMDiff_iff_target]
theorem
smooth_iff_target
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiff I I' n f ↔ Continuous f ∧ ∀ (y : M'), ContMDiffOn I (modelWithCornersSelf 𝕜 E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)
Alias of contMDiff_iff_target.
One can reformulate smoothness as continuity and smoothness in any extended chart in the target.
theorem
contMDiff_zero_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
:
ContMDiff I I' 0 f ↔ Continuous f
zero-smoothness is equivalent to continuity.
Deducing smoothness from smoothness one step beyond #
theorem
ContMDiffWithinAt.of_succ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ}
(h : ContMDiffWithinAt I I' (↑n.succ) f s x)
:
ContMDiffWithinAt I I' (↑n) f s x
theorem
ContMDiffAt.of_succ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ}
(h : ContMDiffAt I I' (↑n.succ) f x)
:
ContMDiffAt I I' (↑n) f x
theorem
ContMDiffOn.of_succ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ}
(h : ContMDiffOn I I' (↑n.succ) f s)
:
ContMDiffOn I I' (↑n) f s
theorem
ContMDiff.of_succ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ}
(h : ContMDiff I I' (↑n.succ) f)
:
ContMDiff I I' (↑n) f
Deducing continuity from smoothness #
theorem
ContMDiffWithinAt.continuousWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(hf : ContMDiffWithinAt I I' n f s x)
:
ContinuousWithinAt f s x
theorem
ContMDiffAt.continuousAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
(hf : ContMDiffAt I I' n f x)
:
ContinuousAt f x
theorem
ContMDiffOn.continuousOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
(hf : ContMDiffOn I I' n f s)
:
ContinuousOn f s
theorem
ContMDiff.continuous
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
(hf : ContMDiff I I' n f)
:
C^∞ smoothness #
theorem
contMDiffWithinAt_top
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
:
ContMDiffWithinAt I I' ⊤ f s x ↔ ∀ (n : ℕ), ContMDiffWithinAt I I' (↑n) f s x
theorem
contMDiffAt_top
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
:
ContMDiffAt I I' ⊤ f x ↔ ∀ (n : ℕ), ContMDiffAt I I' (↑n) f x
theorem
contMDiffOn_top
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
:
ContMDiffOn I I' ⊤ f s ↔ ∀ (n : ℕ), ContMDiffOn I I' (↑n) f s
theorem
contMDiff_top
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
:
theorem
contMDiffWithinAt_iff_nat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContMDiffWithinAt I I' (↑m) f s x
Restriction to a smaller set #
theorem
ContMDiffWithinAt.mono_of_mem_nhdsWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(hf : ContMDiffWithinAt I I' n f s x)
(hts : s ∈ nhdsWithin x t)
:
ContMDiffWithinAt I I' n f t x
@[deprecated ContMDiffWithinAt.mono_of_mem_nhdsWithin]
theorem
ContMDiffWithinAt.mono_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(hf : ContMDiffWithinAt I I' n f s x)
(hts : s ∈ nhdsWithin x t)
:
ContMDiffWithinAt I I' n f t x
Alias of ContMDiffWithinAt.mono_of_mem_nhdsWithin.
theorem
ContMDiffWithinAt.mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(hf : ContMDiffWithinAt I I' n f s x)
(hts : t ⊆ s)
:
ContMDiffWithinAt I I' n f t x
theorem
contMDiffWithinAt_congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(h : s =ᶠ[nhds x] t)
:
ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x
theorem
ContMDiffWithinAt.congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
(hst : s =ᶠ[nhds x] t)
:
ContMDiffWithinAt I I' n f t x
@[deprecated contMDiffWithinAt_congr_set]
theorem
contMDiffWithinAt_congr_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(h : s =ᶠ[nhds x] t)
:
ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x
Alias of contMDiffWithinAt_congr_set.
theorem
contMDiffWithinAt_insert_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x
theorem
ContMDiffWithinAt.of_insert
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
:
ContMDiffWithinAt I I' n f (insert x s) x → ContMDiffWithinAt I I' n f s x
Alias of the forward direction of contMDiffWithinAt_insert_self.
theorem
ContMDiffWithinAt.insert
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
:
ContMDiffWithinAt I I' n f (insert x s) x
theorem
contMDiffWithinAt_congr_set'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(y : M)
(h : s =ᶠ[nhdsWithin x {y}ᶜ] t)
:
ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x
Being C^n in a set only depends on the germ of the set. Version where one only requires
the two sets to coincide locally in the complement of a point y.
theorem
ContMDiffAt.contMDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(hf : ContMDiffAt I I' n f x)
:
ContMDiffWithinAt I I' n f s x
@[deprecated ContMDiffAt.contMDiffWithinAt]
theorem
SmoothAt.smoothWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(hf : ContMDiffAt I I' n f x)
:
ContMDiffWithinAt I I' n f s x
Alias of ContMDiffAt.contMDiffWithinAt.
theorem
ContMDiffOn.mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{n : ℕ∞}
(hf : ContMDiffOn I I' n f s)
(hts : t ⊆ s)
:
ContMDiffOn I I' n f t
theorem
ContMDiff.contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
(hf : ContMDiff I I' n f)
:
ContMDiffOn I I' n f s
@[deprecated ContMDiff.contMDiffOn]
theorem
Smooth.smoothOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
(hf : ContMDiff I I' n f)
:
ContMDiffOn I I' n f s
Alias of ContMDiff.contMDiffOn.
theorem
contMDiffWithinAt_inter'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(ht : t ∈ nhdsWithin x s)
:
ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x
theorem
contMDiffWithinAt_inter
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s t : Set M}
{x : M}
{n : ℕ∞}
(ht : t ∈ nhds x)
:
ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x
theorem
ContMDiffWithinAt.contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
(ht : s ∈ nhds x)
:
ContMDiffAt I I' n f x
@[deprecated ContMDiffWithinAt.contMDiffAt]
theorem
SmoothWithinAt.smoothAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
(ht : s ∈ nhds x)
:
ContMDiffAt I I' n f x
Alias of ContMDiffWithinAt.contMDiffAt.
theorem
ContMDiffOn.contMDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffOn I I' n f s)
(hx : s ∈ nhds x)
:
ContMDiffAt I I' n f x
@[deprecated ContMDiffOn.contMDiffAt]
theorem
SmoothOn.smoothAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffOn I I' n f s)
(hx : s ∈ nhds x)
:
ContMDiffAt I I' n f x
Alias of ContMDiffOn.contMDiffAt.
theorem
contMDiffOn_iff_source_of_mem_maximalAtlas
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : PartialHomeomorph M H}
{f : M → M'}
{s : Set M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
(he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M)
(hs : s ⊆ e.source)
:
ContMDiffOn I I' n f s ↔ ContMDiffOn (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
theorem
contMDiffWithinAt_iff_contMDiffOn_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{n : ℕ}
:
ContMDiffWithinAt I I' (↑n) f s x ↔ ∃ u ∈ nhdsWithin x (insert x s), ContMDiffOn 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
ContMDiffWithinAt.contMDiffOn'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{m : ℕ}
(hm : ↑m ≤ n)
(h : ContMDiffWithinAt I I' n f s x)
:
If a function is C^m within a set at a point, for some finite m, then it is C^m within
this set on an open set around the basepoint.
theorem
ContMDiffWithinAt.contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{m : ℕ}
(hm : ↑m ≤ n)
(h : ContMDiffWithinAt I I' n f s x)
:
∃ u ∈ nhdsWithin x (insert x s), u ⊆ insert x s ∧ ContMDiffOn I I' (↑m) f u
If a function is C^m within a set at a point, for some finite m, then it is C^m within
this set on a neighborhood of the basepoint.
theorem
contMDiffAt_iff_contMDiffOn_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{n : ℕ}
:
ContMDiffAt I I' (↑n) f x ↔ ∃ u ∈ nhds x, ContMDiffOn 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
contMDiffAt_iff_contMDiffAt_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{n : ℕ}
:
ContMDiffAt I I' (↑n) f x ↔ ∀ᶠ (x' : M) in nhds x, ContMDiffAt 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.
theorem
contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{n : ℕ}
:
ContMDiffWithinAt I I' (↑n) f s x ↔ ∀ᶠ (x' : M) in nhdsWithin x (insert x s), ContMDiffWithinAt I I' (↑n) f s 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
ContMDiffWithinAt.congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
(h₁ : ∀ y ∈ s, f₁ y = f y)
(hx : f₁ x = f x)
:
ContMDiffWithinAt I I' n f₁ s x
theorem
contMDiffWithinAt_congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h₁ : ∀ y ∈ s, f₁ y = f y)
(hx : f₁ x = f x)
:
ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x
theorem
ContMDiffWithinAt.congr_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
(h₁ : ∀ y ∈ s, f₁ y = f y)
(hx : x ∈ s)
:
ContMDiffWithinAt I I' n f₁ s x
theorem
contMDiffWithinAt_congr_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h₁ : ∀ y ∈ s, f₁ y = f y)
(hx : x ∈ s)
:
ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x
theorem
ContMDiffWithinAt.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : f₁ x = f x)
:
ContMDiffWithinAt I I' n f₁ s x
theorem
ContMDiffWithinAt.congr_of_eventuallyEq_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h : ContMDiffWithinAt I I' n f s x)
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : x ∈ s)
:
ContMDiffWithinAt I I' n f₁ s x
theorem
Filter.EventuallyEq.contMDiffWithinAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{x : M}
{n : ℕ∞}
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : f₁ x = f x)
:
ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x
theorem
ContMDiffAt.congr_of_eventuallyEq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{x : M}
{n : ℕ∞}
(h : ContMDiffAt I I' n f x)
(h₁ : f₁ =ᶠ[nhds x] f)
:
ContMDiffAt I I' n f₁ x
theorem
Filter.EventuallyEq.contMDiffAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{x : M}
{n : ℕ∞}
(h₁ : f₁ =ᶠ[nhds x] f)
:
ContMDiffAt I I' n f₁ x ↔ ContMDiffAt I I' n f x
theorem
ContMDiffOn.congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{n : ℕ∞}
(h : ContMDiffOn I I' n f s)
(h₁ : ∀ y ∈ s, f₁ y = f y)
:
ContMDiffOn I I' n f₁ s
theorem
contMDiffOn_congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s : Set M}
{n : ℕ∞}
(h₁ : ∀ y ∈ s, f₁ y = f y)
:
ContMDiffOn I I' n f₁ s ↔ ContMDiffOn I I' n f s
theorem
ContMDiffOn.congr_mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f f₁ : M → M'}
{s s₁ : Set M}
{n : ℕ∞}
(hf : ContMDiffOn I I' n f s)
(h₁ : ∀ y ∈ s₁, f₁ y = f y)
(hs : s₁ ⊆ s)
:
ContMDiffOn I I' n f₁ s₁
Locality #
theorem
contMDiffOn_of_locally_contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{n : ℕ∞}
(h : ∀ x ∈ s, ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f (s ∩ u))
:
ContMDiffOn I I' n f s
Being C^n is a local property.
theorem
contMDiff_of_locally_contMDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{n : ℕ∞}
(h : ∀ (x : M), ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f u)
:
ContMDiff I I' n f