The derivative of functions between smooth manifolds #
Let M and M' be two smooth manifolds with corners over a field π (with respective models with
corners I on (E, H) and I' on (E', H')), and let f : M β M'. We define the
derivative of the function at a point, within a set or along the whole space, mimicking the API
for (FrΓ©chet) derivatives. It is denoted by mfderiv I I' f x, where "m" stands for "manifold" and
"f" for "FrΓ©chet" (as in the usual derivative fderiv π f x).
Main definitions #
UniqueMDiffOn I s: predicate saying that, at each point of the sets, a function can have at most one derivative. This technical condition is important when we definemfderivWithinbelow, as otherwise there is an arbitrary choice in the derivative, and many properties will fail (for instance the chain rule). This is analogous toUniqueDiffOn π sin a vector space.
Let f be a map between smooth manifolds. The following definitions follow the fderiv API.
mfderiv I I' f x: the derivative offatx, as a continuous linear map from the tangent space atxto the tangent space atf x. If the map is not differentiable, this is0.mfderivWithin I I' f s x: the derivative offatxwithins, as a continuous linear map from the tangent space atxto the tangent space atf x. If the map is not differentiable withins, this is0.MDifferentiableAt I I' f x: Prop expressing whetherfis differentiable atx.MDifferentiableWithinAt π f s x: Prop expressing whetherfis differentiable withinsatx.HasMFDerivAt I I' f s x f': Prop expressing whetherfhasf'as a derivative atx.HasMFDerivWithinAt I I' f s x f': Prop expressing whetherfhasf'as a derivative withinsatx.MDifferentiableOn I I' f s: Prop expressing thatfis differentiable on the sets.MDifferentiable I I' f: Prop expressing thatfis differentiable everywhere.tangentMap I I' f: the derivative off, as a map from the tangent bundle ofMto the tangent bundle ofM'.
We also establish results on the differential of the identity, constant functions, charts, extended charts. For functions between vector spaces, we show that the usual notions and the manifold notions coincide.
Implementation notes #
The tangent bundle is constructed using the machinery of topological fiber bundles, for which one
can define bundled morphisms and construct canonically maps from the total space of one bundle to
the total space of another one. One could use this mechanism to construct directly the derivative
of a smooth map. However, we want to define the derivative of any map (and let it be zero if the map
is not differentiable) to avoid proof arguments everywhere. This means we have to go back to the
details of the definition of the total space of a fiber bundle constructed from core, to cook up a
suitable definition of the derivative. It is the following: at each point, we have a preferred chart
(used to identify the fiber above the point with the model vector space in fiber bundles). Then one
should read the function using these preferred charts at x and f x, and take the derivative
of f in these charts.
Due to the fact that we are working in a model with corners, with an additional embedding I of the
model space H in the model vector space E, the charts taking values in E are not the original
charts of the manifold, but those ones composed with I, called extended charts. We define
writtenInExtChartAt I I' x f for the function f written in the preferred extended charts. Then
the manifold derivative of f, at x, is just the usual derivative of
writtenInExtChartAt I I' x f, at the point (extChartAt I x) x.
There is a subtelty with respect to continuity: if the function is not continuous, then the image
of a small open set around x will not be contained in the source of the preferred chart around
f x, which means that when reading f in the chart one is losing some information. To avoid this,
we include continuity in the definition of differentiablity (which is reasonable since with any
definition, differentiability implies continuity).
Warning: the derivative (even within a subset) is a linear map on the whole tangent space. Suppose
that one is given a smooth submanifold N, and a function which is smooth on N (i.e., its
restriction to the subtype N is smooth). Then, in the whole manifold M, the property
MDifferentiableOn I I' f N holds. However, mfderivWithin I I' f N is not uniquely defined
(what values would one choose for vectors that are transverse to N?), which can create issues down
the road. The problem here is that knowing the value of f along N does not determine the
differential of f in all directions. This is in contrast to the case where N would be an open
subset, or a submanifold with boundary of maximal dimension, where this issue does not appear.
The predicate UniqueMDiffOn I N indicates that the derivative along N is unique if it exists,
and is an assumption in most statements requiring a form of uniqueness.
On a vector space, the manifold derivative and the usual derivative are equal. This means in particular that they live on the same space, i.e., the tangent space is defeq to the original vector space. To get this property is a motivation for our definition of the tangent space as a single copy of the vector space, instead of more usual definitions such as the space of derivations, or the space of equivalence classes of smooth curves in the manifold.
Tags #
Derivative, manifold
Derivative of maps between manifolds #
The derivative of a smooth map f between smooth manifold M and M' at x is a bounded linear
map from the tangent space to M at x, to the tangent space to M' at f x. Since we defined
the tangent space using one specific chart, the formula for the derivative is written in terms of
this specific chart.
We use the names MDifferentiable and mfderiv, where the prefix letter m means "manifold".
def
DifferentiableWithinAtProp
{π : 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')
(f : H β H')
(s : Set H)
(x : H)
:
Property in the model space of a model with corners of being differentiable within at set at a point, when read in the model vector space. This property will be lifted to manifolds to define differentiable functions between manifolds.
Equations
- DifferentiableWithinAtProp I I' f s x = DifferentiableWithinAt π (βI' β f β β(ModelWithCorners.symm I)) (β(ModelWithCorners.symm I) β»ΒΉ' s β© Set.range βI) (βI x)
Instances For
theorem
differentiable_within_at_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')
:
Being differentiable in the model space is a local property, invariant under smooth maps. Therefore, it will lift nicely to manifolds.
def
UniqueMDiffWithinAt
{π : 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]
(s : Set M)
(x : M)
:
Predicate ensuring that, at a point and within a set, a function can have at most one derivative. This is expressed using the preferred chart at the considered point.
Equations
- UniqueMDiffWithinAt I s x = UniqueDiffWithinAt π (β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s β© Set.range βI) (β(extChartAt I x) x)
Instances For
def
UniqueMDiffOn
{π : 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]
(s : Set M)
:
Predicate ensuring that, at all points of a set, a function can have at most one derivative.
Equations
- UniqueMDiffOn I s = β x β s, UniqueMDiffWithinAt I s x
Instances For
def
MDifferentiableWithinAt
{π : 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)
:
MDifferentiableWithinAt I I' f s x indicates that the function f between manifolds
has a derivative at the point x within the set s.
This is a generalization of DifferentiableWithinAt to manifolds.
We require continuity in the definition, as otherwise points close to x in s could be sent by
f outside of the chart domain around f x. Then the chart could do anything to the image points,
and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while
this would not mean anything relevant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
mdifferentiableWithinAt_iff_liftPropWithinAt
{π : 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)
:
MDifferentiableWithinAt I I' f s x β ChartedSpace.LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x
def
MDifferentiableAt
{π : 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)
:
MDifferentiableAt I I' f x indicates that the function f between manifolds
has a derivative at the point x.
This is a generalization of DifferentiableAt to manifolds.
We require continuity in the definition, as otherwise points close to x could be sent by
f outside of the chart domain around f x. Then the chart could do anything to the image points,
and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while
this would not mean anything relevant.
Equations
- MDifferentiableAt I I' f x = (ContinuousAt f x β§ DifferentiableWithinAt π (writtenInExtChartAt I I' x f) (Set.range βI) (β(extChartAt I x) x))
Instances For
theorem
mdifferentiableAt_iff_liftPropAt
{π : 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)
:
MDifferentiableAt I I' f x β ChartedSpace.LiftPropAt (DifferentiableWithinAtProp I I') f x
def
MDifferentiableOn
{π : 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)
:
MDifferentiableOn I I' f s indicates that the function f between manifolds
has a derivative within s at all points of s.
This is a generalization of DifferentiableOn to manifolds.
Equations
- MDifferentiableOn I I' f s = β x β s, MDifferentiableWithinAt I I' f s x
Instances For
def
MDifferentiable
{π : 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')
:
MDifferentiable I I' f indicates that the function f between manifolds
has a derivative everywhere.
This is a generalization of Differentiable to manifolds.
Equations
- MDifferentiable I I' f = β (x : M), MDifferentiableAt I I' f x
Instances For
def
PartialHomeomorph.MDifferentiable
{π : 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 : PartialHomeomorph M M')
:
Prop registering if a local homeomorphism is a local diffeomorphism on its source
Equations
- PartialHomeomorph.MDifferentiable I I' f = (MDifferentiableOn I I' (βf) f.source β§ MDifferentiableOn I' I (β(PartialHomeomorph.symm f)) f.target)
Instances For
def
HasMFDerivWithinAt
{π : 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']
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(f : M β M')
(s : Set M)
(x : M)
(f' : TangentSpace I x βL[π] TangentSpace I' (f x))
:
HasMFDerivWithinAt I I' f s x f' indicates that the function f between manifolds
has, at the point x and within the set s, the derivative f'. Here, f' is a continuous linear
map from the tangent space at x to the tangent space at f x.
This is a generalization of HasFDerivWithinAt to manifolds (as indicated by the prefix m).
The order of arguments is changed as the type of the derivative f' depends on the choice of x.
We require continuity in the definition, as otherwise points close to x in s could be sent by
f outside of the chart domain around f x. Then the chart could do anything to the image points,
and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while
this would not mean anything relevant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HasMFDerivAt
{π : 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']
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(f : M β M')
(x : M)
(f' : TangentSpace I x βL[π] TangentSpace I' (f x))
:
HasMFDerivAt I I' f x f' indicates that the function f between manifolds
has, at the point x, the derivative f'. Here, f' is a continuous linear
map from the tangent space at x to the tangent space at f x.
We require continuity in the definition, as otherwise points close to x s could be sent by
f outside of the chart domain around f x. Then the chart could do anything to the image points,
and in particular by coincidence writtenInExtChartAt I I' x f could be differentiable, while
this would not mean anything relevant.
Equations
- HasMFDerivAt I I' f x f' = (ContinuousAt f x β§ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' (Set.range βI) (β(extChartAt I x) x))
Instances For
def
mfderivWithin
{π : 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']
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(f : M β M')
(s : Set M)
(x : M)
:
TangentSpace I x βL[π] TangentSpace I' (f x)
Let f be a function between two smooth manifolds. Then mfderivWithin I I' f s x is the
derivative of f at x within s, as a continuous linear map from the tangent space at x to the
tangent space at f x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
mfderiv
{π : 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']
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(f : M β M')
(x : M)
:
TangentSpace I x βL[π] TangentSpace I' (f x)
Let f be a function between two smooth manifolds. Then mfderiv I I' f x is the derivative of
f at x, as a continuous linear map from the tangent space at x to the tangent space at
f x.
Equations
- mfderiv I I' f x = if MDifferentiableAt I I' f x then fderivWithin π (writtenInExtChartAt I I' x f) (Set.range βI) (β(extChartAt I x) x) else 0
Instances For
def
tangentMapWithin
{π : 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']
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(f : M β M')
(s : Set M)
:
TangentBundle I M β TangentBundle I' M'
The derivative within a set, as a map between the tangent bundles
Equations
- tangentMapWithin I I' f s p = { proj := f p.proj, snd := (mfderivWithin I I' f s p.proj) p.snd }
Instances For
def
tangentMap
{π : 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']
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
(f : M β M')
:
TangentBundle I M β TangentBundle I' M'
The derivative, as a map between the tangent bundles
Equations
- tangentMap I I' f p = { proj := f p.proj, snd := (mfderiv I I' f p.proj) p.snd }
Instances For
Unique differentiability sets in manifolds #
theorem
uniqueMDiffWithinAt_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]
{x : M}
:
UniqueMDiffWithinAt I Set.univ x
theorem
uniqueMDiffWithinAt_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]
{s : Set M}
{x : M}
:
UniqueMDiffWithinAt I s x β UniqueDiffWithinAt π (β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s β© (extChartAt I x).target) (β(extChartAt I x) x)
theorem
UniqueMDiffWithinAt.mono_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]
{s : Set M}
{t : Set M}
{x : M}
(hs : UniqueMDiffWithinAt I s x)
(ht : nhdsWithin x s β€ nhdsWithin x t)
:
UniqueMDiffWithinAt I t x
theorem
UniqueMDiffWithinAt.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]
{s : Set M}
{t : Set M}
{x : M}
(hs : UniqueMDiffWithinAt I s x)
(ht : t β nhdsWithin x s)
:
UniqueMDiffWithinAt I t x
theorem
UniqueMDiffWithinAt.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]
{x : M}
{s : Set M}
{t : Set M}
(h : UniqueMDiffWithinAt I s x)
(st : s β t)
:
UniqueMDiffWithinAt I t x
theorem
UniqueMDiffWithinAt.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]
{x : M}
{s : Set M}
{t : Set M}
(hs : UniqueMDiffWithinAt I s x)
(ht : t β nhdsWithin x s)
:
UniqueMDiffWithinAt I (s β© t) x
theorem
UniqueMDiffWithinAt.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]
{x : M}
{s : Set M}
{t : Set M}
(hs : UniqueMDiffWithinAt I s x)
(ht : t β nhds x)
:
UniqueMDiffWithinAt I (s β© t) x
theorem
IsOpen.uniqueMDiffWithinAt
{π : 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]
{x : M}
{s : Set M}
(xs : x β s)
(hs : IsOpen s)
:
UniqueMDiffWithinAt I s x
theorem
UniqueMDiffOn.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]
{s : Set M}
{t : Set M}
(hs : UniqueMDiffOn I s)
(ht : IsOpen t)
:
UniqueMDiffOn I (s β© t)
theorem
IsOpen.uniqueMDiffOn
{π : 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]
{s : Set M}
(hs : IsOpen s)
:
UniqueMDiffOn I s
theorem
uniqueMDiffOn_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]
:
UniqueMDiffOn I Set.univ
theorem
UniqueMDiffWithinAt.eq
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
{fβ' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(U : UniqueMDiffWithinAt I s x)
(h : HasMFDerivWithinAt I I' f s x f')
(hβ : HasMFDerivWithinAt I I' f s x fβ')
:
f' = fβ'
UniqueMDiffWithinAt achieves its goal: it implies the uniqueness of the derivative.
theorem
UniqueMDiffOn.eq
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
{fβ' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(U : UniqueMDiffOn I s)
(hx : x β s)
(h : HasMFDerivWithinAt I I' f s x f')
(hβ : HasMFDerivWithinAt I I' f s x fβ')
:
f' = fβ'
theorem
UniqueMDiffWithinAt.prod
{π : 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']
{x : M}
{y : M'}
{s : Set M}
{t : Set M'}
(hs : UniqueMDiffWithinAt I s x)
(ht : UniqueMDiffWithinAt I' t y)
:
UniqueMDiffWithinAt (ModelWithCorners.prod I I') (s ΓΛ’ t) (x, y)
theorem
UniqueMDiffOn.prod
{π : 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']
{s : Set M}
{t : Set M'}
(hs : UniqueMDiffOn I s)
(ht : UniqueMDiffOn I' t)
:
UniqueMDiffOn (ModelWithCorners.prod I I') (s ΓΛ’ t)
General lemmas on derivatives of functions between manifolds #
We mimick the API for functions between vector spaces
theorem
mdifferentiableWithinAt_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}
:
MDifferentiableWithinAt I I' f s x β ContinuousWithinAt f s x β§ DifferentiableWithinAt π (writtenInExtChartAt I I' x f)
((extChartAt I x).target β© β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s) (β(extChartAt I x) x)
theorem
mdifferentiableWithinAt_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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{x' : M}
{y : M'}
(hx : x' β (chartAt H x).toPartialEquiv.source)
(hy : f x' β (chartAt H' y).toPartialEquiv.source)
:
MDifferentiableWithinAt I I' f s x' β ContinuousWithinAt f s x' β§ DifferentiableWithinAt π (β(extChartAt I' y) β f β β(PartialEquiv.symm (extChartAt I x)))
(β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s β© Set.range βI) (β(extChartAt I x) x')
One can reformulate differentiability within a set at a point as continuity within this set at this point, and differentiability in any chart containing that point.
theorem
mfderivWithin_zero_of_not_mdifferentiableWithinAt
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : Β¬MDifferentiableWithinAt I I' f s x)
:
mfderivWithin I I' f s x = 0
theorem
mfderiv_zero_of_not_mdifferentiableAt
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : Β¬MDifferentiableAt I I' f x)
:
theorem
HasMFDerivWithinAt.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'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f t x f')
(hst : s β t)
:
HasMFDerivWithinAt I I' f s x f'
theorem
HasMFDerivAt.hasMFDerivWithinAt
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivAt I I' f x f')
:
HasMFDerivWithinAt I I' f s x f'
theorem
HasMFDerivWithinAt.mdifferentiableWithinAt
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f s x f')
:
MDifferentiableWithinAt I I' f s x
theorem
HasMFDerivAt.mdifferentiableAt
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivAt I I' f x f')
:
MDifferentiableAt I I' f x
@[simp]
theorem
hasMFDerivWithinAt_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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
:
HasMFDerivWithinAt I I' f Set.univ x f' β HasMFDerivAt I I' f x f'
theorem
hasMFDerivAt_unique
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{fβ' : TangentSpace I x βL[π] TangentSpace I' (f x)}
{fβ' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(hβ : HasMFDerivAt I I' f x fβ')
(hβ : HasMFDerivAt I I' f x fβ')
:
fβ' = fβ'
theorem
hasMFDerivWithinAt_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'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : t β nhdsWithin x s)
:
HasMFDerivWithinAt I I' f (s β© t) x f' β HasMFDerivWithinAt I I' f s x f'
theorem
hasMFDerivWithinAt_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'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : t β nhds x)
:
HasMFDerivWithinAt I I' f (s β© t) x f' β HasMFDerivWithinAt I I' f s x f'
theorem
HasMFDerivWithinAt.union
{π : 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}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(hs : HasMFDerivWithinAt I I' f s x f')
(ht : HasMFDerivWithinAt I I' f t x f')
:
HasMFDerivWithinAt I I' f (s βͺ t) x f'
theorem
HasMFDerivWithinAt.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'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f s x f')
(ht : s β nhdsWithin x t)
:
HasMFDerivWithinAt I I' f t x f'
theorem
HasMFDerivWithinAt.hasMFDerivAt
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f s x f')
(hs : s β nhds x)
:
HasMFDerivAt I I' f x f'
theorem
MDifferentiableWithinAt.hasMFDerivWithinAt
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableWithinAt I I' f s x)
:
HasMFDerivWithinAt I I' f s x (mfderivWithin I I' f s x)
theorem
MDifferentiableWithinAt.mfderivWithin
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableWithinAt I I' f s x)
:
mfderivWithin I I' f s x = fderivWithin π (writtenInExtChartAt I I' x f) (β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s β© Set.range βI)
(β(extChartAt I x) x)
theorem
MDifferentiableAt.hasMFDerivAt
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableAt I I' f x)
:
HasMFDerivAt I I' f x (mfderiv I I' f x)
theorem
MDifferentiableAt.mfderiv
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableAt I I' f x)
:
mfderiv I I' f x = fderivWithin π (writtenInExtChartAt I I' x f) (Set.range βI) (β(extChartAt I x) x)
theorem
HasMFDerivAt.mfderiv
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivAt I I' f x f')
:
theorem
HasMFDerivWithinAt.mfderivWithin
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f s x f')
(hxs : UniqueMDiffWithinAt I s x)
:
mfderivWithin I I' f s x = f'
theorem
MDifferentiable.mfderivWithin
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableAt I I' f x)
(hxs : UniqueMDiffWithinAt I s x)
:
mfderivWithin I I' f s x = mfderiv I I' f x
theorem
mfderivWithin_subset
{π : 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}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(st : s β t)
(hs : UniqueMDiffWithinAt I s x)
(h : MDifferentiableWithinAt I I' f t x)
:
mfderivWithin I I' f s x = mfderivWithin I I' f t x
theorem
MDifferentiableWithinAt.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'}
{x : M}
{s : Set M}
{t : Set M}
(hst : s β t)
(h : MDifferentiableWithinAt I I' f t x)
:
MDifferentiableWithinAt I I' f s x
theorem
mdifferentiableWithinAt_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}
:
MDifferentiableWithinAt I I' f Set.univ x β MDifferentiableAt I I' f x
theorem
mdifferentiableWithinAt_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'}
{x : M}
{s : Set M}
{t : Set M}
(ht : t β nhds x)
:
MDifferentiableWithinAt I I' f (s β© t) x β MDifferentiableWithinAt I I' f s x
theorem
mdifferentiableWithinAt_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'}
{x : M}
{s : Set M}
{t : Set M}
(ht : t β nhdsWithin x s)
:
MDifferentiableWithinAt I I' f (s β© t) x β MDifferentiableWithinAt I I' f s x
theorem
MDifferentiableAt.mdifferentiableWithinAt
{π : 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}
{s : Set M}
(h : MDifferentiableAt I I' f x)
:
MDifferentiableWithinAt I I' f s x
theorem
MDifferentiableWithinAt.mdifferentiableAt
{π : 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}
{s : Set M}
(h : MDifferentiableWithinAt I I' f s x)
(hs : s β nhds x)
:
MDifferentiableAt I I' f x
theorem
MDifferentiableOn.mdifferentiableAt
{π : 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}
{s : Set M}
(h : MDifferentiableOn I I' f s)
(hx : s β nhds x)
:
MDifferentiableAt I I' f x
theorem
MDifferentiableOn.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 : Set M}
{t : Set M}
(h : MDifferentiableOn I I' f t)
(st : s β t)
:
MDifferentiableOn I I' f s
theorem
mdifferentiableOn_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'}
:
MDifferentiableOn I I' f Set.univ β MDifferentiable I I' f
theorem
MDifferentiable.mdifferentiableOn
{π : 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}
(h : MDifferentiable I I' f)
:
MDifferentiableOn I I' f s
theorem
mdifferentiableOn_of_locally_mdifferentiableOn
{π : 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}
(h : β x β s, β (u : Set M), IsOpen u β§ x β u β§ MDifferentiableOn I I' f (s β© u))
:
MDifferentiableOn I I' f s
@[simp]
theorem
mfderivWithin_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'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
:
mfderivWithin I I' f Set.univ = mfderiv I I' f
theorem
mfderivWithin_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'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(ht : t β nhds x)
:
mfderivWithin I I' f (s β© t) x = mfderivWithin I I' f s x
theorem
mfderivWithin_of_mem_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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : s β nhds x)
:
mfderivWithin I I' f s x = mfderiv I I' f x
theorem
mfderivWithin_of_isOpen
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(hs : IsOpen s)
(hx : x β s)
:
mfderivWithin I I' f s x = mfderiv I I' f x
theorem
mfderivWithin_eq_mfderiv
{π : 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}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(hs : UniqueMDiffWithinAt I s x)
(h : MDifferentiableAt I I' f x)
:
mfderivWithin I I' f s x = mfderiv I I' f x
theorem
mdifferentiableAt_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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{x' : M}
{y : M'}
(hx : x' β (chartAt H x).toPartialEquiv.source)
(hy : f x' β (chartAt H' y).toPartialEquiv.source)
:
MDifferentiableAt I I' f x' β ContinuousAt f x' β§ DifferentiableWithinAt π (β(extChartAt I' y) β f β β(PartialEquiv.symm (extChartAt I x))) (Set.range βI)
(β(extChartAt I x) x')
Deducing differentiability from smoothness #
theorem
ContMDiffWithinAt.mdifferentiableWithinAt
{π : 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}
{s : Set M}
{n : ββ}
(hf : ContMDiffWithinAt I I' n f s x)
(hn : 1 β€ n)
:
MDifferentiableWithinAt I I' f s x
theorem
ContMDiffAt.mdifferentiableAt
{π : 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)
(hn : 1 β€ n)
:
MDifferentiableAt I I' f x
theorem
ContMDiffOn.mdifferentiableOn
{π : 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)
(hn : 1 β€ n)
:
MDifferentiableOn I I' f s
theorem
ContMDiff.mdifferentiable
{π : 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)
(hn : 1 β€ n)
:
MDifferentiable I I' f
theorem
SmoothWithinAt.mdifferentiableWithinAt
{π : 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}
{s : Set M}
(hf : SmoothWithinAt I I' f s x)
:
MDifferentiableWithinAt I I' f s x
theorem
SmoothAt.mdifferentiableAt
{π : 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}
(hf : SmoothAt I I' f x)
:
MDifferentiableAt I I' f x
theorem
SmoothOn.mdifferentiableOn
{π : 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}
(hf : SmoothOn I I' f s)
:
MDifferentiableOn I I' f s
theorem
Smooth.mdifferentiable
{π : 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'}
(hf : Smooth I I' f)
:
MDifferentiable I I' f
theorem
Smooth.mdifferentiableAt
{π : 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}
(hf : Smooth I I' f)
:
MDifferentiableAt I I' f x
theorem
Smooth.mdifferentiableWithinAt
{π : 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}
{s : Set M}
(hf : Smooth I I' f)
:
MDifferentiableWithinAt I I' f s x
Deriving continuity from differentiability on manifolds #
theorem
HasMFDerivWithinAt.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'}
{x : M}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f s x f')
:
ContinuousWithinAt f s x
theorem
HasMFDerivAt.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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivAt I I' f x f')
:
ContinuousAt f x
theorem
MDifferentiableWithinAt.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'}
{x : M}
{s : Set M}
(h : MDifferentiableWithinAt I I' f s x)
:
ContinuousWithinAt f s x
theorem
MDifferentiableAt.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}
(h : MDifferentiableAt I I' f x)
:
ContinuousAt f x
theorem
MDifferentiableOn.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}
(h : MDifferentiableOn I I' f s)
:
ContinuousOn f s
theorem
MDifferentiable.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'}
(h : MDifferentiable I I' f)
:
theorem
tangentMapWithin_subset
{π : 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}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{p : TangentBundle I M}
(st : s β t)
(hs : UniqueMDiffWithinAt I s p.proj)
(h : MDifferentiableWithinAt I I' f t p.proj)
:
tangentMapWithin I I' f s p = tangentMapWithin I I' f t p
theorem
tangentMapWithin_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'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
:
tangentMapWithin I I' f Set.univ = tangentMap I I' f
theorem
tangentMapWithin_eq_tangentMap
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{p : TangentBundle I M}
(hs : UniqueMDiffWithinAt I s p.proj)
(h : MDifferentiableAt I I' f p.proj)
:
tangentMapWithin I I' f s p = tangentMap I I' f p
@[simp]
theorem
tangentMapWithin_proj
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{p : TangentBundle I M}
:
(tangentMapWithin I I' f s p).proj = f p.proj
@[simp]
theorem
tangentMap_proj
{π : 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'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{p : TangentBundle I M}
:
(tangentMap I I' f p).proj = f p.proj
theorem
MDifferentiableWithinAt.prod_mk
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{x : M}
{s : Set M}
{f : M β M'}
{g : M β M''}
(hf : MDifferentiableWithinAt I I' f s x)
(hg : MDifferentiableWithinAt I I'' g s x)
:
MDifferentiableWithinAt I (ModelWithCorners.prod I' I'') (fun (x : M) => (f x, g x)) s x
theorem
MDifferentiableAt.prod_mk
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{x : M}
{f : M β M'}
{g : M β M''}
(hf : MDifferentiableAt I I' f x)
(hg : MDifferentiableAt I I'' g x)
:
MDifferentiableAt I (ModelWithCorners.prod I' I'') (fun (x : M) => (f x, g x)) x
theorem
MDifferentiableOn.prod_mk
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{s : Set M}
{f : M β M'}
{g : M β M''}
(hf : MDifferentiableOn I I' f s)
(hg : MDifferentiableOn I I'' g s)
:
MDifferentiableOn I (ModelWithCorners.prod I' I'') (fun (x : M) => (f x, g x)) s
theorem
MDifferentiable.prod_mk
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{g : M β M''}
(hf : MDifferentiable I I' f)
(hg : MDifferentiable I I'' g)
:
MDifferentiable I (ModelWithCorners.prod I' I'') fun (x : M) => (f x, g x)
theorem
MDifferentiableWithinAt.prod_mk_space
{π : 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']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{x : M}
{s : Set M}
{f : M β E'}
{g : M β E''}
(hf : MDifferentiableWithinAt I (modelWithCornersSelf π E') f s x)
(hg : MDifferentiableWithinAt I (modelWithCornersSelf π E'') g s x)
:
MDifferentiableWithinAt I (modelWithCornersSelf π (E' Γ E'')) (fun (x : M) => (f x, g x)) s x
theorem
MDifferentiableAt.prod_mk_space
{π : 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']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{x : M}
{f : M β E'}
{g : M β E''}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f x)
(hg : MDifferentiableAt I (modelWithCornersSelf π E'') g x)
:
MDifferentiableAt I (modelWithCornersSelf π (E' Γ E'')) (fun (x : M) => (f x, g x)) x
theorem
MDifferentiableOn.prod_mk_space
{π : 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']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{s : Set M}
{f : M β E'}
{g : M β E''}
(hf : MDifferentiableOn I (modelWithCornersSelf π E') f s)
(hg : MDifferentiableOn I (modelWithCornersSelf π E'') g s)
:
MDifferentiableOn I (modelWithCornersSelf π (E' Γ E'')) (fun (x : M) => (f x, g x)) s
theorem
MDifferentiable.prod_mk_space
{π : 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']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{f : M β E'}
{g : M β E''}
(hf : MDifferentiable I (modelWithCornersSelf π E') f)
(hg : MDifferentiable I (modelWithCornersSelf π E'') g)
:
MDifferentiable I (modelWithCornersSelf π (E' Γ E'')) fun (x : M) => (f x, g x)
Congruence lemmas for derivatives on manifolds #
theorem
HasMFDerivWithinAt.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 : M β M'}
{fβ : M β M'}
{x : M}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f s x f')
(hβ : fβ =αΆ [nhdsWithin x s] f)
(hx : fβ x = f x)
:
HasMFDerivWithinAt I I' fβ s x f'
theorem
HasMFDerivWithinAt.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 : M β M'}
{fβ : M β M'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivWithinAt I I' f s x f')
(ht : β x β t, fβ x = f x)
(hx : fβ x = f x)
(hβ : t β s)
:
HasMFDerivWithinAt I I' fβ t x f'
theorem
HasMFDerivAt.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 : M β M'}
{fβ : M β M'}
{x : M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
(h : HasMFDerivAt I I' f x f')
(hβ : fβ =αΆ [nhds x] f)
:
HasMFDerivAt I I' fβ x f'
theorem
MDifferentiableWithinAt.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 : M β M'}
{fβ : M β M'}
{x : M}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableWithinAt I I' f s x)
(hβ : fβ =αΆ [nhdsWithin x s] f)
(hx : fβ x = f x)
:
MDifferentiableWithinAt I I' fβ s x
theorem
Filter.EventuallyEq.mdifferentiableWithinAt_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'}
{fβ : M β M'}
{x : M}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(hβ : fβ =αΆ [nhdsWithin x s] f)
(hx : fβ x = f x)
:
MDifferentiableWithinAt I I' f s x β MDifferentiableWithinAt I I' fβ s x
theorem
MDifferentiableWithinAt.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 : M β M'}
{fβ : M β M'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableWithinAt I I' f s x)
(ht : β x β t, fβ x = f x)
(hx : fβ x = f x)
(hβ : t β s)
:
MDifferentiableWithinAt I I' fβ t x
theorem
MDifferentiableWithinAt.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 : M β M'}
{fβ : M β M'}
{x : M}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableWithinAt I I' f s x)
(ht : β x β s, fβ x = f x)
(hx : fβ x = f x)
:
MDifferentiableWithinAt I I' fβ s x
theorem
MDifferentiableOn.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 : M β M'}
{fβ : M β M'}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableOn I I' f s)
(h' : β x β t, fβ x = f x)
(hβ : t β s)
:
MDifferentiableOn I I' fβ t
theorem
MDifferentiableAt.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 : M β M'}
{fβ : M β M'}
{x : M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableAt I I' f x)
(hL : fβ =αΆ [nhds x] f)
:
MDifferentiableAt I I' fβ x
theorem
MDifferentiableWithinAt.mfderivWithin_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 : M β M'}
{fβ : M β M'}
{x : M}
{s : Set M}
{t : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : MDifferentiableWithinAt I I' f s x)
(hs : β x β t, fβ x = f x)
(hx : fβ x = f x)
(hxt : UniqueMDiffWithinAt I t x)
(hβ : t β s)
:
mfderivWithin I I' fβ t x = mfderivWithin I I' f s x
theorem
Filter.EventuallyEq.mfderivWithin_eq
{π : 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'}
{fβ : M β M'}
{x : M}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(hs : UniqueMDiffWithinAt I s x)
(hL : fβ =αΆ [nhdsWithin x s] f)
(hx : fβ x = f x)
:
mfderivWithin I I' fβ s x = mfderivWithin I I' f s x
theorem
mfderivWithin_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 : M β M'}
{fβ : M β M'}
{x : M}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(hs : UniqueMDiffWithinAt I s x)
(hL : β x β s, fβ x = f x)
(hx : fβ x = f x)
:
mfderivWithin I I' fβ s x = mfderivWithin I I' f s x
theorem
tangentMapWithin_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 : M β M'}
{fβ : M β M'}
{s : Set M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(h : β x β s, f x = fβ x)
(p : TangentBundle I M)
(hp : p.proj β s)
(hs : UniqueMDiffWithinAt I s p.proj)
:
tangentMapWithin I I' f s p = tangentMapWithin I I' fβ s p
theorem
Filter.EventuallyEq.mfderiv_eq
{π : 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'}
{fβ : M β M'}
{x : M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
(hL : fβ =αΆ [nhds x] f)
:
theorem
mfderiv_congr_point
{π : 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}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{x' : M}
(h : x = x')
:
A congruence lemma for mfderiv, (ab)using the fact that TangentSpace I' (f x) is
definitionally equal to E'.
theorem
mfderiv_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 : M β M'}
{x : M}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
{f' : M β M'}
(h : f = f')
:
A congruence lemma for mfderiv, (ab)using the fact that TangentSpace I' (f x) is
definitionally equal to E'.
Composition lemmas #
theorem
writtenInExtChartAt_comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{x : M}
{s : Set M}
{g : M' β M''}
(h : ContinuousWithinAt f s x)
:
{y : E |
writtenInExtChartAt I I'' x (g β f) y = (writtenInExtChartAt I' I'' (f x) g β writtenInExtChartAt I I' x f) y} β nhdsWithin (β(extChartAt I x) x) (β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s β© Set.range βI)
theorem
HasMFDerivWithinAt.comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
(x : M)
{s : Set M}
{g : M' β M''}
{u : Set M'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
{g' : TangentSpace I' (f x) βL[π] TangentSpace I'' (g (f x))}
(hg : HasMFDerivWithinAt I' I'' g u (f x) g')
(hf : HasMFDerivWithinAt I I' f s x f')
(hst : s β f β»ΒΉ' u)
:
HasMFDerivWithinAt I I'' (g β f) s x (ContinuousLinearMap.comp g' f')
theorem
HasMFDerivAt.comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
(x : M)
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
{g' : TangentSpace I' (f x) βL[π] TangentSpace I'' (g (f x))}
(hg : HasMFDerivAt I' I'' g (f x) g')
(hf : HasMFDerivAt I I' f x f')
:
HasMFDerivAt I I'' (g β f) x (ContinuousLinearMap.comp g' f')
The chain rule for manifolds.
theorem
HasMFDerivAt.comp_hasMFDerivWithinAt
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
(x : M)
{s : Set M}
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
{f' : TangentSpace I x βL[π] TangentSpace I' (f x)}
{g' : TangentSpace I' (f x) βL[π] TangentSpace I'' (g (f x))}
(hg : HasMFDerivAt I' I'' g (f x) g')
(hf : HasMFDerivWithinAt I I' f s x f')
:
HasMFDerivWithinAt I I'' (g β f) s x (ContinuousLinearMap.comp g' f')
theorem
MDifferentiableWithinAt.comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
(x : M)
{s : Set M}
{g : M' β M''}
{u : Set M'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(hg : MDifferentiableWithinAt I' I'' g u (f x))
(hf : MDifferentiableWithinAt I I' f s x)
(h : s β f β»ΒΉ' u)
:
MDifferentiableWithinAt I I'' (g β f) s x
theorem
MDifferentiableAt.comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
(x : M)
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(hg : MDifferentiableAt I' I'' g (f x))
(hf : MDifferentiableAt I I' f x)
:
MDifferentiableAt I I'' (g β f) x
theorem
mfderivWithin_comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
(x : M)
{s : Set M}
{g : M' β M''}
{u : Set M'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(hg : MDifferentiableWithinAt I' I'' g u (f x))
(hf : MDifferentiableWithinAt I I' f s x)
(h : s β f β»ΒΉ' u)
(hxs : UniqueMDiffWithinAt I s x)
:
mfderivWithin I I'' (g β f) s x = ContinuousLinearMap.comp (mfderivWithin I' I'' g u (f x)) (mfderivWithin I I' f s x)
theorem
mfderiv_comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
(x : M)
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(hg : MDifferentiableAt I' I'' g (f x))
(hf : MDifferentiableAt I I' f x)
:
theorem
mfderiv_comp_of_eq
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
{x : M}
{y : M'}
(hg : MDifferentiableAt I' I'' g y)
(hf : MDifferentiableAt I I' f x)
(hy : f x = y)
:
theorem
MDifferentiableOn.comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{s : Set M}
{g : M' β M''}
{u : Set M'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(hg : MDifferentiableOn I' I'' g u)
(hf : MDifferentiableOn I I' f s)
(st : s β f β»ΒΉ' u)
:
MDifferentiableOn I I'' (g β f) s
theorem
MDifferentiable.comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(hg : MDifferentiable I' I'' g)
(hf : MDifferentiable I I' f)
:
MDifferentiable I I'' (g β f)
theorem
tangentMapWithin_comp_at
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{s : Set M}
{g : M' β M''}
{u : Set M'}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(p : TangentBundle I M)
(hg : MDifferentiableWithinAt I' I'' g u (f p.proj))
(hf : MDifferentiableWithinAt I I' f s p.proj)
(h : s β f β»ΒΉ' u)
(hps : UniqueMDiffWithinAt I s p.proj)
:
tangentMapWithin I I'' (g β f) s p = tangentMapWithin I' I'' g u (tangentMapWithin I I' f s p)
theorem
tangentMap_comp_at
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(p : TangentBundle I M)
(hg : MDifferentiableAt I' I'' g (f p.proj))
(hf : MDifferentiableAt I I' f p.proj)
:
tangentMap I I'' (g β f) p = tangentMap I' I'' g (tangentMap I I' f p)
theorem
tangentMap_comp
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{f : M β M'}
{g : M' β M''}
[Is : SmoothManifoldWithCorners I M]
[I's : SmoothManifoldWithCorners I' M']
[I''s : SmoothManifoldWithCorners I'' M'']
(hg : MDifferentiable I' I'' g)
(hf : MDifferentiable I I' f)
:
tangentMap I I'' (g β f) = tangentMap I' I'' g β tangentMap I I' f
Relations between vector space derivative and manifold derivative #
The manifold derivative mfderiv, when considered on the model vector space with its trivial
manifold structure, coincides with the usual Frechet derivative fderiv. In this section, we prove
this and related statements.
theorem
uniqueMDiffWithinAt_iff_uniqueDiffWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{s : Set E}
{x : E}
:
UniqueMDiffWithinAt (modelWithCornersSelf π E) s x β UniqueDiffWithinAt π s x
theorem
UniqueMDiffWithinAt.uniqueDiffWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{s : Set E}
{x : E}
:
UniqueMDiffWithinAt (modelWithCornersSelf π E) s x β UniqueDiffWithinAt π s x
Alias of the forward direction of uniqueMDiffWithinAt_iff_uniqueDiffWithinAt.
theorem
UniqueDiffWithinAt.uniqueMDiffWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{s : Set E}
{x : E}
:
UniqueDiffWithinAt π s x β UniqueMDiffWithinAt (modelWithCornersSelf π E) s x
Alias of the reverse direction of uniqueMDiffWithinAt_iff_uniqueDiffWithinAt.
theorem
uniqueMDiffOn_iff_uniqueDiffOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{s : Set E}
:
UniqueMDiffOn (modelWithCornersSelf π E) s β UniqueDiffOn π s
theorem
UniqueMDiffOn.uniqueDiffOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{s : Set E}
:
UniqueMDiffOn (modelWithCornersSelf π E) s β UniqueDiffOn π s
Alias of the forward direction of uniqueMDiffOn_iff_uniqueDiffOn.
theorem
UniqueDiffOn.uniqueMDiffOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{s : Set E}
:
UniqueDiffOn π s β UniqueMDiffOn (modelWithCornersSelf π E) s
Alias of the reverse direction of uniqueMDiffOn_iff_uniqueDiffOn.
theorem
writtenInExtChartAt_model_space
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
:
writtenInExtChartAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') x f = f
theorem
hasMFDerivWithinAt_iff_hasFDerivWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
{x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)}
:
HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x f' β HasFDerivWithinAt f f' s x
theorem
HasMFDerivWithinAt.hasFDerivWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
{x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)}
:
HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x f' β HasFDerivWithinAt f f' s x
Alias of the forward direction of hasMFDerivWithinAt_iff_hasFDerivWithinAt.
theorem
HasFDerivWithinAt.hasMFDerivWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
{x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)}
:
HasFDerivWithinAt f f' s x β HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x f'
Alias of the reverse direction of hasMFDerivWithinAt_iff_hasFDerivWithinAt.
theorem
hasMFDerivAt_iff_hasFDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)}
:
HasMFDerivAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x f' β HasFDerivAt f f' x
theorem
HasMFDerivAt.hasFDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)}
:
HasMFDerivAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x f' β HasFDerivAt f f' x
Alias of the forward direction of hasMFDerivAt_iff_hasFDerivAt.
theorem
HasFDerivAt.hasMFDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
{f' : TangentSpace (modelWithCornersSelf π E) x βL[π] TangentSpace (modelWithCornersSelf π E') (f x)}
:
HasFDerivAt f f' x β HasMFDerivAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x f'
Alias of the reverse direction of hasMFDerivAt_iff_hasFDerivAt.
theorem
mdifferentiableWithinAt_iff_differentiableWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
{x : E}
:
MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x β DifferentiableWithinAt π f s x
For maps between vector spaces, MDifferentiableWithinAt and DifferentiableWithinAt
coincide
theorem
DifferentiableWithinAt.mdifferentiableWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
{x : E}
:
DifferentiableWithinAt π f s x β MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x
Alias of the reverse direction of mdifferentiableWithinAt_iff_differentiableWithinAt.
For maps between vector spaces, MDifferentiableWithinAt and DifferentiableWithinAt
coincide
theorem
MDifferentiableWithinAt.differentiableWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
{x : E}
:
MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x β DifferentiableWithinAt π f s x
Alias of the forward direction of mdifferentiableWithinAt_iff_differentiableWithinAt.
For maps between vector spaces, MDifferentiableWithinAt and DifferentiableWithinAt
coincide
theorem
mdifferentiableAt_iff_differentiableAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
:
MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x β DifferentiableAt π f x
For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide
theorem
DifferentiableAt.mdifferentiableAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
:
DifferentiableAt π f x β MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x
Alias of the reverse direction of mdifferentiableAt_iff_differentiableAt.
For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide
theorem
MDifferentiableAt.differentiableAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
:
MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x β DifferentiableAt π f x
Alias of the forward direction of mdifferentiableAt_iff_differentiableAt.
For maps between vector spaces, MDifferentiableAt and DifferentiableAt coincide
theorem
mdifferentiableOn_iff_differentiableOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
:
MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s β DifferentiableOn π f s
For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide
theorem
MDifferentiableOn.differentiableOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
:
MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s β DifferentiableOn π f s
Alias of the forward direction of mdifferentiableOn_iff_differentiableOn.
For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide
theorem
DifferentiableOn.mdifferentiableOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
:
DifferentiableOn π f s β MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s
Alias of the reverse direction of mdifferentiableOn_iff_differentiableOn.
For maps between vector spaces, MDifferentiableOn and DifferentiableOn coincide
theorem
mdifferentiable_iff_differentiable
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
:
MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') f β Differentiable π f
For maps between vector spaces, MDifferentiable and Differentiable coincide
theorem
Differentiable.mdifferentiable
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
:
Differentiable π f β MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') f
Alias of the reverse direction of mdifferentiable_iff_differentiable.
For maps between vector spaces, MDifferentiable and Differentiable coincide
theorem
MDifferentiable.differentiable
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
:
MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') f β Differentiable π f
Alias of the forward direction of mdifferentiable_iff_differentiable.
For maps between vector spaces, MDifferentiable and Differentiable coincide
@[simp]
theorem
mfderivWithin_eq_fderivWithin
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{s : Set E}
{x : E}
:
mfderivWithin (modelWithCornersSelf π E) (modelWithCornersSelf π E') f s x = fderivWithin π f s x
For maps between vector spaces, mfderivWithin and fderivWithin coincide
@[simp]
theorem
mfderiv_eq_fderiv
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : E β E'}
{x : E}
:
mfderiv (modelWithCornersSelf π E) (modelWithCornersSelf π E') f x = fderiv π f x
Differentiability of specific functions #
theorem
ContinuousLinearMap.hasMFDerivWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
{x : E}
:
HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s x f
theorem
ContinuousLinearMap.hasMFDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{x : E}
:
HasMFDerivAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) x f
theorem
ContinuousLinearMap.mdifferentiableWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
{x : E}
:
MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s x
theorem
ContinuousLinearMap.mdifferentiableOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
:
MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s
theorem
ContinuousLinearMap.mdifferentiableAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{x : E}
:
MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) x
theorem
ContinuousLinearMap.mdifferentiable
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
:
MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') βf
theorem
ContinuousLinearMap.mfderiv_eq
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{x : E}
:
mfderiv (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) x = f
theorem
ContinuousLinearMap.mfderivWithin_eq
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
{x : E}
(hs : UniqueMDiffWithinAt (modelWithCornersSelf π E) s x)
:
mfderivWithin (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s x = f
theorem
ContinuousLinearEquiv.hasMFDerivWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
{x : E}
:
HasMFDerivWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s x βf
theorem
ContinuousLinearEquiv.hasMFDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{x : E}
:
HasMFDerivAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) x βf
theorem
ContinuousLinearEquiv.mdifferentiableWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
{x : E}
:
MDifferentiableWithinAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s x
theorem
ContinuousLinearEquiv.mdifferentiableOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
:
MDifferentiableOn (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s
theorem
ContinuousLinearEquiv.mdifferentiableAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{x : E}
:
MDifferentiableAt (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) x
theorem
ContinuousLinearEquiv.mdifferentiable
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
:
MDifferentiable (modelWithCornersSelf π E) (modelWithCornersSelf π E') βf
theorem
ContinuousLinearEquiv.mfderiv_eq
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{x : E}
:
mfderiv (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) x = βf
theorem
ContinuousLinearEquiv.mfderivWithin_eq
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : E βL[π] E')
{s : Set E}
{x : E}
(hs : UniqueMDiffWithinAt (modelWithCornersSelf π E) s x)
:
mfderivWithin (modelWithCornersSelf π E) (modelWithCornersSelf π E') (βf) s x = βf
Identity #
theorem
hasMFDerivAt_id
{π : 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]
[SmoothManifoldWithCorners I M]
(x : M)
:
HasMFDerivAt I I id x (ContinuousLinearMap.id π (TangentSpace I x))
theorem
hasMFDerivWithinAt_id
{π : 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]
[SmoothManifoldWithCorners I M]
(s : Set M)
(x : M)
:
HasMFDerivWithinAt I I id s x (ContinuousLinearMap.id π (TangentSpace I x))
theorem
mdifferentiableAt_id
{π : 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]
[SmoothManifoldWithCorners I M]
{x : M}
:
MDifferentiableAt I I id x
theorem
mdifferentiableWithinAt_id
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{x : M}
:
MDifferentiableWithinAt I I id s x
theorem
mdifferentiable_id
{π : 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]
[SmoothManifoldWithCorners I M]
:
MDifferentiable I I id
theorem
mdifferentiableOn_id
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
:
MDifferentiableOn I I id s
@[simp]
theorem
mfderiv_id
{π : 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]
[SmoothManifoldWithCorners I M]
{x : M}
:
mfderiv I I id x = ContinuousLinearMap.id π (TangentSpace I x)
theorem
mfderivWithin_id
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{x : M}
(hxs : UniqueMDiffWithinAt I s x)
:
mfderivWithin I I id s x = ContinuousLinearMap.id π (TangentSpace I x)
@[simp]
theorem
tangentMap_id
{π : 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]
[SmoothManifoldWithCorners I M]
:
tangentMap I I id = id
theorem
tangentMapWithin_id
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{p : TangentBundle I M}
(hs : UniqueMDiffWithinAt I s p.proj)
:
tangentMapWithin I I id s p = p
Constants #
theorem
hasMFDerivAt_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
(c : M')
(x : M)
:
HasMFDerivAt I I' (fun (x : M) => c) x 0
theorem
hasMFDerivWithinAt_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
(c : M')
(s : Set M)
(x : M)
:
HasMFDerivWithinAt I I' (fun (x : M) => c) s x 0
theorem
mdifferentiableAt_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{x : M}
{c : M'}
:
MDifferentiableAt I I' (fun (x : M) => c) x
theorem
mdifferentiableWithinAt_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
{x : M}
{c : M'}
:
MDifferentiableWithinAt I I' (fun (x : M) => c) s x
theorem
mdifferentiable_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{c : M'}
:
MDifferentiable I I' fun (x : M) => c
theorem
mdifferentiableOn_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
{c : M'}
:
MDifferentiableOn I I' (fun (x : M) => c) s
@[simp]
theorem
mfderiv_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{x : M}
{c : M'}
:
theorem
mfderivWithin_const
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
{x : M}
{c : M'}
(hxs : UniqueMDiffWithinAt I s x)
:
mfderivWithin I I' (fun (x : M) => c) s x = 0
Operations on the product of two manifolds #
theorem
hasMFDerivAt_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
(x : M Γ M')
:
HasMFDerivAt (ModelWithCorners.prod I I') I Prod.fst x
(ContinuousLinearMap.fst π (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
hasMFDerivWithinAt_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
(s : Set (M Γ M'))
(x : M Γ M')
:
HasMFDerivWithinAt (ModelWithCorners.prod I I') I Prod.fst s x
(ContinuousLinearMap.fst π (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
mdifferentiableAt_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{x : M Γ M'}
:
MDifferentiableAt (ModelWithCorners.prod I I') I Prod.fst x
theorem
mdifferentiableWithinAt_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
{x : M Γ M'}
:
MDifferentiableWithinAt (ModelWithCorners.prod I I') I Prod.fst s x
theorem
mdifferentiable_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
:
MDifferentiable (ModelWithCorners.prod I I') I Prod.fst
theorem
mdifferentiableOn_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
:
MDifferentiableOn (ModelWithCorners.prod I I') I Prod.fst s
@[simp]
theorem
mfderiv_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{x : M Γ M'}
:
mfderiv (ModelWithCorners.prod I I') I Prod.fst x = ContinuousLinearMap.fst π (TangentSpace I x.1) (TangentSpace I' x.2)
theorem
mfderivWithin_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
{x : M Γ M'}
(hxs : UniqueMDiffWithinAt (ModelWithCorners.prod I I') s x)
:
mfderivWithin (ModelWithCorners.prod I I') I Prod.fst s x = ContinuousLinearMap.fst π (TangentSpace I x.1) (TangentSpace I' x.2)
@[simp]
theorem
tangentMap_prod_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{p : TangentBundle (ModelWithCorners.prod I I') (M Γ M')}
:
tangentMap (ModelWithCorners.prod I I') I Prod.fst p = { proj := p.proj.1, snd := p.snd.1 }
theorem
tangentMapWithin_prod_fst
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
{p : TangentBundle (ModelWithCorners.prod I I') (M Γ M')}
(hs : UniqueMDiffWithinAt (ModelWithCorners.prod I I') s p.proj)
:
tangentMapWithin (ModelWithCorners.prod I I') I Prod.fst s p = { proj := p.proj.1, snd := p.snd.1 }
theorem
hasMFDerivAt_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
(x : M Γ M')
:
HasMFDerivAt (ModelWithCorners.prod I I') I' Prod.snd x
(ContinuousLinearMap.snd π (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
hasMFDerivWithinAt_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
(s : Set (M Γ M'))
(x : M Γ M')
:
HasMFDerivWithinAt (ModelWithCorners.prod I I') I' Prod.snd s x
(ContinuousLinearMap.snd π (TangentSpace I x.1) (TangentSpace I' x.2))
theorem
mdifferentiableAt_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{x : M Γ M'}
:
MDifferentiableAt (ModelWithCorners.prod I I') I' Prod.snd x
theorem
mdifferentiableWithinAt_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
{x : M Γ M'}
:
MDifferentiableWithinAt (ModelWithCorners.prod I I') I' Prod.snd s x
theorem
mdifferentiable_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
:
MDifferentiable (ModelWithCorners.prod I I') I' Prod.snd
theorem
mdifferentiableOn_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
:
MDifferentiableOn (ModelWithCorners.prod I I') I' Prod.snd s
@[simp]
theorem
mfderiv_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{x : M Γ M'}
:
mfderiv (ModelWithCorners.prod I I') I' Prod.snd x = ContinuousLinearMap.snd π (TangentSpace I x.1) (TangentSpace I' x.2)
theorem
mfderivWithin_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
{x : M Γ M'}
(hxs : UniqueMDiffWithinAt (ModelWithCorners.prod I I') s x)
:
mfderivWithin (ModelWithCorners.prod I I') I' Prod.snd s x = ContinuousLinearMap.snd π (TangentSpace I x.1) (TangentSpace I' x.2)
@[simp]
theorem
tangentMap_prod_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{p : TangentBundle (ModelWithCorners.prod I I') (M Γ M')}
:
tangentMap (ModelWithCorners.prod I I') I' Prod.snd p = { proj := p.proj.2, snd := p.snd.2 }
theorem
tangentMapWithin_prod_snd
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set (M Γ M')}
{p : TangentBundle (ModelWithCorners.prod I I') (M Γ M')}
(hs : UniqueMDiffWithinAt (ModelWithCorners.prod I I') s p.proj)
:
tangentMapWithin (ModelWithCorners.prod I I') I' Prod.snd s p = { proj := p.proj.2, snd := p.snd.2 }
theorem
MDifferentiableAt.mfderiv_prod
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[SmoothManifoldWithCorners I'' M'']
{f : M β M'}
{g : M β M''}
{x : M}
(hf : MDifferentiableAt I I' f x)
(hg : MDifferentiableAt I I'' g x)
:
mfderiv I (ModelWithCorners.prod I' I'') (fun (x : M) => (f x, g x)) x = ContinuousLinearMap.prod (mfderiv I I' f x) (mfderiv I I'' g x)
theorem
mfderiv_prod_left
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{xβ : M}
{yβ : M'}
:
mfderiv I (ModelWithCorners.prod I I') (fun (x : M) => (x, yβ)) xβ = ContinuousLinearMap.inl π (TangentSpace I xβ) (TangentSpace I' yβ)
theorem
mfderiv_prod_right
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{xβ : M}
{yβ : M'}
:
mfderiv I' (ModelWithCorners.prod I I') (fun (y : M') => (xβ, y)) yβ = ContinuousLinearMap.inr π (TangentSpace I xβ) (TangentSpace I' yβ)
theorem
mfderiv_prod_eq_add
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
(I'' : ModelWithCorners π E'' H'')
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
[SmoothManifoldWithCorners I'' M'']
{f : M Γ M' β M''}
{p : M Γ M'}
(hf : MDifferentiableAt (ModelWithCorners.prod I I') I'' f p)
:
mfderiv (ModelWithCorners.prod I I') I'' f p = let_fun this :=
mfderiv (ModelWithCorners.prod I I') I'' (fun (z : M Γ M') => f (z.1, p.2)) p + mfderiv (ModelWithCorners.prod I I') I'' (fun (z : M Γ M') => f (p.1, z.2)) p;
this
The total derivative of a function in two variables is the sum of the partial derivatives.
Note that to state this (without casts) we need to be able to see through the definition of
TangentSpace.
Arithmetic #
Note that in the HasMFDerivAt lemmas there is an abuse of the defeq between E' and
TangentSpace π(π, E') (f z) (similarly for g',F',p',q'). In general this defeq is not
canonical, but in this case (the tangent space of a vector space) it is canonical.
theorem
HasMFDerivAt.add
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{g : M β E'}
{f' : TangentSpace I z βL[π] E'}
{g' : TangentSpace I z βL[π] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf π E') f z f')
(hg : HasMFDerivAt I (modelWithCornersSelf π E') g z g')
:
HasMFDerivAt I (modelWithCornersSelf π E') (f + g) z (f' + g')
theorem
MDifferentiableAt.add
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{g : M β E'}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf π E') g z)
:
MDifferentiableAt I (modelWithCornersSelf π E') (f + g) z
theorem
MDifferentiable.add
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : M β E'}
{g : M β E'}
(hf : MDifferentiable I (modelWithCornersSelf π E') f)
(hg : MDifferentiable I (modelWithCornersSelf π E') g)
:
MDifferentiable I (modelWithCornersSelf π E') (f + g)
theorem
mfderiv_add
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{g : M β E'}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf π E') g z)
:
mfderiv I (modelWithCornersSelf π E') (f + g) z = mfderiv I (modelWithCornersSelf π E') f z + mfderiv I (modelWithCornersSelf π E') g z
theorem
HasMFDerivAt.const_smul
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{f' : TangentSpace I z βL[π] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf π E') f z f')
(s : π)
:
HasMFDerivAt I (modelWithCornersSelf π E') (s β’ f) z (s β’ f')
theorem
MDifferentiableAt.const_smul
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f z)
(s : π)
:
MDifferentiableAt I (modelWithCornersSelf π E') (s β’ f) z
theorem
MDifferentiable.const_smul
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : M β E'}
(s : π)
(hf : MDifferentiable I (modelWithCornersSelf π E') f)
:
MDifferentiable I (modelWithCornersSelf π E') (s β’ f)
theorem
const_smul_mfderiv
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f z)
(s : π)
:
mfderiv I (modelWithCornersSelf π E') (s β’ f) z = s β’ mfderiv I (modelWithCornersSelf π E') f z
theorem
HasMFDerivAt.neg
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{f' : TangentSpace I z βL[π] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf π E') f z f')
:
HasMFDerivAt I (modelWithCornersSelf π E') (-f) z (-f')
theorem
hasMFDerivAt_neg
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{f' : TangentSpace I z βL[π] E'}
:
HasMFDerivAt I (modelWithCornersSelf π E') (-f) z (-f') β HasMFDerivAt I (modelWithCornersSelf π E') f z f'
theorem
MDifferentiableAt.neg
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f z)
:
MDifferentiableAt I (modelWithCornersSelf π E') (-f) z
theorem
mdifferentiableAt_neg
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
:
MDifferentiableAt I (modelWithCornersSelf π E') (-f) z β MDifferentiableAt I (modelWithCornersSelf π E') f z
theorem
MDifferentiable.neg
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : M β E'}
(hf : MDifferentiable I (modelWithCornersSelf π E') f)
:
MDifferentiable I (modelWithCornersSelf π E') (-f)
theorem
mfderiv_neg
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
(f : M β E')
(x : M)
:
mfderiv I (modelWithCornersSelf π E') (-f) x = -mfderiv I (modelWithCornersSelf π E') f x
theorem
HasMFDerivAt.sub
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{g : M β E'}
{f' : TangentSpace I z βL[π] E'}
{g' : TangentSpace I z βL[π] E'}
(hf : HasMFDerivAt I (modelWithCornersSelf π E') f z f')
(hg : HasMFDerivAt I (modelWithCornersSelf π E') g z g')
:
HasMFDerivAt I (modelWithCornersSelf π E') (f - g) z (f' - g')
theorem
MDifferentiableAt.sub
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{g : M β E'}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf π E') g z)
:
MDifferentiableAt I (modelWithCornersSelf π E') (f - g) z
theorem
MDifferentiable.sub
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{f : M β E'}
{g : M β E'}
(hf : MDifferentiable I (modelWithCornersSelf π E') f)
(hg : MDifferentiable I (modelWithCornersSelf π E') g)
:
MDifferentiable I (modelWithCornersSelf π E') (f - g)
theorem
mfderiv_sub
{π : 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]
[SmoothManifoldWithCorners I M]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace π E']
{z : M}
{f : M β E'}
{g : M β E'}
(hf : MDifferentiableAt I (modelWithCornersSelf π E') f z)
(hg : MDifferentiableAt I (modelWithCornersSelf π E') g z)
:
mfderiv I (modelWithCornersSelf π E') (f - g) z = mfderiv I (modelWithCornersSelf π E') f z - mfderiv I (modelWithCornersSelf π E') g z
theorem
HasMFDerivWithinAt.mul'
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
{p' : TangentSpace I z βL[π] F'}
{q' : TangentSpace I z βL[π] F'}
(hp : HasMFDerivWithinAt I (modelWithCornersSelf π F') p s z p')
(hq : HasMFDerivWithinAt I (modelWithCornersSelf π F') q s z q')
:
HasMFDerivWithinAt I (modelWithCornersSelf π F') (p * q) s z (p z β’ q' + ContinuousLinearMap.smulRight p' (q z))
theorem
HasMFDerivAt.mul'
{π : 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]
[SmoothManifoldWithCorners I M]
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
{p' : TangentSpace I z βL[π] F'}
{q' : TangentSpace I z βL[π] F'}
(hp : HasMFDerivAt I (modelWithCornersSelf π F') p z p')
(hq : HasMFDerivAt I (modelWithCornersSelf π F') q z q')
:
HasMFDerivAt I (modelWithCornersSelf π F') (p * q) z (p z β’ q' + ContinuousLinearMap.smulRight p' (q z))
theorem
MDifferentiableWithinAt.mul
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
(hp : MDifferentiableWithinAt I (modelWithCornersSelf π F') p s z)
(hq : MDifferentiableWithinAt I (modelWithCornersSelf π F') q s z)
:
MDifferentiableWithinAt I (modelWithCornersSelf π F') (p * q) s z
theorem
MDifferentiableAt.mul
{π : 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]
[SmoothManifoldWithCorners I M]
{z : M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
(hp : MDifferentiableAt I (modelWithCornersSelf π F') p z)
(hq : MDifferentiableAt I (modelWithCornersSelf π F') q z)
:
MDifferentiableAt I (modelWithCornersSelf π F') (p * q) z
theorem
MDifferentiableOn.mul
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
(hp : MDifferentiableOn I (modelWithCornersSelf π F') p s)
(hq : MDifferentiableOn I (modelWithCornersSelf π F') q s)
:
MDifferentiableOn I (modelWithCornersSelf π F') (p * q) s
theorem
MDifferentiable.mul
{π : 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]
[SmoothManifoldWithCorners I M]
{F' : Type u_11}
[NormedRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
(hp : MDifferentiable I (modelWithCornersSelf π F') p)
(hq : MDifferentiable I (modelWithCornersSelf π F') q)
:
MDifferentiable I (modelWithCornersSelf π F') (p * q)
theorem
HasMFDerivWithinAt.mul
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{z : M}
{F' : Type u_11}
[NormedCommRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
{p' : TangentSpace I z βL[π] F'}
{q' : TangentSpace I z βL[π] F'}
(hp : HasMFDerivWithinAt I (modelWithCornersSelf π F') p s z p')
(hq : HasMFDerivWithinAt I (modelWithCornersSelf π F') q s z q')
:
HasMFDerivWithinAt I (modelWithCornersSelf π F') (p * q) s z (p z β’ q' + q z β’ p')
theorem
HasMFDerivAt.mul
{π : 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]
[SmoothManifoldWithCorners I M]
{z : M}
{F' : Type u_11}
[NormedCommRing F']
[NormedAlgebra π F']
{p : M β F'}
{q : M β F'}
{p' : TangentSpace I z βL[π] F'}
{q' : TangentSpace I z βL[π] F'}
(hp : HasMFDerivAt I (modelWithCornersSelf π F') p z p')
(hq : HasMFDerivAt I (modelWithCornersSelf π F') q z q')
:
HasMFDerivAt I (modelWithCornersSelf π F') (p * q) z (p z β’ q' + q z β’ p')
Model with corners #
theorem
ModelWithCorners.hasMFDerivAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
{x : H}
:
HasMFDerivAt I (modelWithCornersSelf π E) (βI) x (ContinuousLinearMap.id π (TangentSpace I x))
theorem
ModelWithCorners.hasMFDerivWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
{s : Set H}
{x : H}
:
HasMFDerivWithinAt I (modelWithCornersSelf π E) (βI) s x (ContinuousLinearMap.id π (TangentSpace I x))
theorem
ModelWithCorners.mdifferentiableWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
{s : Set H}
{x : H}
:
MDifferentiableWithinAt I (modelWithCornersSelf π E) (βI) s x
theorem
ModelWithCorners.mdifferentiableAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
{x : H}
:
MDifferentiableAt I (modelWithCornersSelf π E) (βI) x
theorem
ModelWithCorners.mdifferentiableOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
{s : Set H}
:
MDifferentiableOn I (modelWithCornersSelf π E) (βI) s
theorem
ModelWithCorners.mdifferentiable
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
:
MDifferentiable I (modelWithCornersSelf π E) βI
theorem
ModelWithCorners.hasMFDerivWithinAt_symm
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
{x : E}
(hx : x β Set.range βI)
:
HasMFDerivWithinAt (modelWithCornersSelf π E) I (β(ModelWithCorners.symm I)) (Set.range βI) x
(ContinuousLinearMap.id π (TangentSpace (modelWithCornersSelf π E) x))
theorem
ModelWithCorners.mdifferentiableOn_symm
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners π E H)
:
MDifferentiableOn (modelWithCornersSelf π E) I (β(ModelWithCorners.symm I)) (Set.range βI)
theorem
mdifferentiableAt_atlas
{π : 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]
[SmoothManifoldWithCorners I M]
{e : PartialHomeomorph M H}
(h : e β atlas H M)
{x : M}
(hx : x β e.source)
:
MDifferentiableAt I I (βe) x
theorem
mdifferentiableOn_atlas
{π : 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]
[SmoothManifoldWithCorners I M]
{e : PartialHomeomorph M H}
(h : e β atlas H M)
:
MDifferentiableOn I I (βe) e.source
theorem
mdifferentiableAt_atlas_symm
{π : 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]
[SmoothManifoldWithCorners I M]
{e : PartialHomeomorph M H}
(h : e β atlas H M)
{x : H}
(hx : x β e.target)
:
MDifferentiableAt I I (β(PartialHomeomorph.symm e)) x
theorem
mdifferentiableOn_atlas_symm
{π : 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]
[SmoothManifoldWithCorners I M]
{e : PartialHomeomorph M H}
(h : e β atlas H M)
:
MDifferentiableOn I I (β(PartialHomeomorph.symm e)) e.target
theorem
mdifferentiable_of_mem_atlas
{π : 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]
[SmoothManifoldWithCorners I M]
{e : PartialHomeomorph M H}
(h : e β atlas H M)
:
theorem
mdifferentiable_chart
{π : 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]
[SmoothManifoldWithCorners I M]
(x : M)
:
PartialHomeomorph.MDifferentiable I I (chartAt H x)
theorem
tangentMap_chart
{π : 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]
[SmoothManifoldWithCorners I M]
{p : TangentBundle I M}
{q : TangentBundle I M}
(h : q.proj β (chartAt H p.proj).toPartialEquiv.source)
:
tangentMap I I (β(chartAt H p.proj)) q = (Bundle.TotalSpace.toProd H E).symm (β(chartAt (ModelProd H E) p) q)
The derivative of the chart at a base point is the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.
theorem
tangentMap_chart_symm
{π : 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]
[SmoothManifoldWithCorners I M]
{p : TangentBundle I M}
{q : TangentBundle I H}
(h : q.proj β (chartAt H p.proj).toPartialEquiv.target)
:
tangentMap I I (β(PartialHomeomorph.symm (chartAt H p.proj))) q = β(PartialHomeomorph.symm (chartAt (ModelProd H E) p)) ((Bundle.TotalSpace.toProd H E) q)
The derivative of the inverse of the chart at a base point is the inverse of the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.
Differentiable local homeomorphisms #
theorem
PartialHomeomorph.MDifferentiable.symm
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
:
theorem
PartialHomeomorph.MDifferentiable.mdifferentiableAt
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
{x : M}
(hx : x β e.source)
:
MDifferentiableAt I I' (βe) x
theorem
PartialHomeomorph.MDifferentiable.mdifferentiableAt_symm
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
{x : M'}
(hx : x β e.target)
:
MDifferentiableAt I' I (β(PartialHomeomorph.symm e)) x
theorem
PartialHomeomorph.MDifferentiable.symm_comp_deriv
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
ContinuousLinearMap.comp (mfderiv I' I (β(PartialHomeomorph.symm e)) (βe x)) (mfderiv I I' (βe) x) = ContinuousLinearMap.id π (TangentSpace I x)
theorem
PartialHomeomorph.MDifferentiable.comp_symm_deriv
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M'}
(hx : x β e.target)
:
ContinuousLinearMap.comp (mfderiv I I' (βe) (β(PartialHomeomorph.symm e) x))
(mfderiv I' I (β(PartialHomeomorph.symm e)) x) = ContinuousLinearMap.id π (TangentSpace I' x)
def
PartialHomeomorph.MDifferentiable.mfderiv
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
TangentSpace I x βL[π] TangentSpace I' (βe x)
The derivative of a differentiable local homeomorphism, as a continuous linear equivalence
between the tangent spaces at x and e x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
PartialHomeomorph.MDifferentiable.mfderiv_bijective
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
Function.Bijective β(mfderiv I I' (βe) x)
theorem
PartialHomeomorph.MDifferentiable.mfderiv_injective
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
Function.Injective β(mfderiv I I' (βe) x)
theorem
PartialHomeomorph.MDifferentiable.mfderiv_surjective
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
Function.Surjective β(mfderiv I I' (βe) x)
theorem
PartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot
{π : 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 M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
LinearMap.ker (mfderiv I I' (βe) x) = β₯
theorem
PartialHomeomorph.MDifferentiable.range_mfderiv_eq_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']
{e : PartialHomeomorph M M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
LinearMap.range (mfderiv I I' (βe) x) = β€
theorem
PartialHomeomorph.MDifferentiable.range_mfderiv_eq_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']
{e : PartialHomeomorph M M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
{x : M}
(hx : x β e.source)
:
theorem
PartialHomeomorph.MDifferentiable.trans
{π : 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'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace π E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners π E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{e : PartialHomeomorph M M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
{e' : PartialHomeomorph M' M''}
[SmoothManifoldWithCorners I M]
[SmoothManifoldWithCorners I' M']
[SmoothManifoldWithCorners I'' M'']
(he' : PartialHomeomorph.MDifferentiable I' I'' e')
:
PartialHomeomorph.MDifferentiable I I'' (PartialHomeomorph.trans e e')
Differentiability of extChartAt #
theorem
hasMFDerivAt_extChartAt
{π : 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]
[SmoothManifoldWithCorners I M]
{x : M}
{y : M}
(h : y β (chartAt H x).toPartialEquiv.source)
:
HasMFDerivAt I (modelWithCornersSelf π E) (β(extChartAt I x)) y (mfderiv I I (β(chartAt H x)) y)
theorem
hasMFDerivWithinAt_extChartAt
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{x : M}
{y : M}
(h : y β (chartAt H x).toPartialEquiv.source)
:
HasMFDerivWithinAt I (modelWithCornersSelf π E) (β(extChartAt I x)) s y (mfderiv I I (β(chartAt H x)) y)
theorem
mdifferentiableAt_extChartAt
{π : 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]
[SmoothManifoldWithCorners I M]
{x : M}
{y : M}
(h : y β (chartAt H x).toPartialEquiv.source)
:
MDifferentiableAt I (modelWithCornersSelf π E) (β(extChartAt I x)) y
theorem
mdifferentiableOn_extChartAt
{π : 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]
[SmoothManifoldWithCorners I M]
{x : M}
:
MDifferentiableOn I (modelWithCornersSelf π E) (β(extChartAt I x)) (chartAt H x).toPartialEquiv.source
Unique derivative sets in manifolds #
theorem
UniqueMDiffWithinAt.image_denseRange
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
{x : M}
(hs : UniqueMDiffWithinAt I s x)
{f : M β M'}
{f' : E βL[π] E'}
(hf : HasMFDerivWithinAt I I' f s x f')
(hd : DenseRange βf')
:
UniqueMDiffWithinAt I' (f '' s) (f x)
If s has the unique differential property at x, f is differentiable within s at xand its derivative has Dense range, thenf '' shas the Unique differential property atf x`.
theorem
UniqueMDiffOn.image_denseRange'
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
(hs : UniqueMDiffOn I s)
{f : M β M'}
{f' : M β E βL[π] E'}
(hf : β x β s, HasMFDerivWithinAt I I' f s x (f' x))
(hd : β x β s, DenseRange β(f' x))
:
UniqueMDiffOn I' (f '' s)
If s has the unique differential, f is differentiable on s and its derivative at every
point of s has dense range, then f '' s has the unique differential property. This version
uses HaMFDerivWithinAt predicate.
theorem
UniqueMDiffOn.image_denseRange
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
(hs : UniqueMDiffOn I s)
{f : M β M'}
(hf : MDifferentiableOn I I' f s)
(hd : β x β s, DenseRange β(mfderivWithin I I' f s x))
:
UniqueMDiffOn I' (f '' s)
If s has the unique differential, f is differentiable on s and its derivative at every
point of s has dense range, then f '' s has the unique differential property.
theorem
UniqueMDiffWithinAt.preimage_localHomeomorph
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
{x : M}
(hs : UniqueMDiffWithinAt I s x)
{e : PartialHomeomorph M M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
(hx : x β e.source)
:
UniqueMDiffWithinAt I' (e.target β© β(PartialHomeomorph.symm e) β»ΒΉ' s) (βe x)
theorem
UniqueMDiffOn.uniqueMDiffOn_preimage
{π : 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]
[SmoothManifoldWithCorners I 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']
[SmoothManifoldWithCorners I' M']
{s : Set M}
(hs : UniqueMDiffOn I s)
{e : PartialHomeomorph M M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
:
UniqueMDiffOn I' (e.target β© β(PartialHomeomorph.symm e) β»ΒΉ' s)
If a set has the unique differential property, then its image under a local diffeomorphism also has the unique differential property.
theorem
UniqueMDiffOn.uniqueDiffOn_target_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]
[SmoothManifoldWithCorners I M]
{s : Set M}
(hs : UniqueMDiffOn I s)
(x : M)
:
UniqueDiffOn π ((extChartAt I x).target β© β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' s)
If a set in a manifold has the unique derivative property, then its pullback by any extended chart, in the vector space, also has the unique derivative property.
theorem
UniqueMDiffOn.uniqueDiffOn_inter_preimage
{π : 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]
[SmoothManifoldWithCorners I 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']
{s : Set M}
(hs : UniqueMDiffOn I s)
(x : M)
(y : M')
{f : M β M'}
(hf : ContinuousOn f s)
:
UniqueDiffOn π
((extChartAt I x).target β© β(PartialEquiv.symm (extChartAt I x)) β»ΒΉ' (s β© f β»ΒΉ' (extChartAt I' y).source))
When considering functions between manifolds, this statement shows up often. It entails the unique differential of the pullback in extended charts of the set where the function can be read in the charts.
theorem
Trivialization.mdifferentiable
{π : 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]
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace π F]
{Z : M β Type u_9}
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) β TopologicalSpace (Z b)]
[(b : M) β AddCommMonoid (Z b)]
[(b : M) β Module π (Z b)]
[FiberBundle F Z]
[VectorBundle π F Z]
[SmoothVectorBundle F Z I]
(e : Trivialization F Bundle.TotalSpace.proj)
[MemTrivializationAtlas e]
:
PartialHomeomorph.MDifferentiable (ModelWithCorners.prod I (modelWithCornersSelf π F))
(ModelWithCorners.prod I (modelWithCornersSelf π F)) e.toPartialHomeomorph
theorem
UniqueMDiffWithinAt.smooth_bundle_preimage
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace π F]
{Z : M β Type u_9}
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) β TopologicalSpace (Z b)]
[(b : M) β AddCommMonoid (Z b)]
[(b : M) β Module π (Z b)]
[FiberBundle F Z]
[VectorBundle π F Z]
[SmoothVectorBundle F Z I]
{p : Bundle.TotalSpace F Z}
(hs : UniqueMDiffWithinAt I s p.proj)
:
UniqueMDiffWithinAt (ModelWithCorners.prod I (modelWithCornersSelf π F)) (Bundle.TotalSpace.proj β»ΒΉ' s) p
theorem
UniqueMDiffWithinAt.smooth_bundle_preimage'
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace π F]
(Z : M β Type u_9)
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) β TopologicalSpace (Z b)]
[(b : M) β AddCommMonoid (Z b)]
[(b : M) β Module π (Z b)]
[FiberBundle F Z]
[VectorBundle π F Z]
[SmoothVectorBundle F Z I]
{b : M}
(hs : UniqueMDiffWithinAt I s b)
(x : Z b)
:
UniqueMDiffWithinAt (ModelWithCorners.prod I (modelWithCornersSelf π F)) (Bundle.TotalSpace.proj β»ΒΉ' s)
{ proj := b, snd := x }
theorem
UniqueMDiffOn.smooth_bundle_preimage
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
{F : Type u_8}
[NormedAddCommGroup F]
[NormedSpace π F]
(Z : M β Type u_9)
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) β TopologicalSpace (Z b)]
[(b : M) β AddCommMonoid (Z b)]
[(b : M) β Module π (Z b)]
[FiberBundle F Z]
[VectorBundle π F Z]
[SmoothVectorBundle F Z I]
(hs : UniqueMDiffOn I s)
:
UniqueMDiffOn (ModelWithCorners.prod I (modelWithCornersSelf π F)) (Bundle.TotalSpace.proj β»ΒΉ' s)
In a smooth fiber bundle, the preimage under the projection of a set with unique differential in the basis also has unique differential.
theorem
UniqueMDiffOn.tangentBundle_proj_preimage
{π : 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]
[SmoothManifoldWithCorners I M]
{s : Set M}
(hs : UniqueMDiffOn I s)
:
UniqueMDiffOn (ModelWithCorners.tangent I) (Bundle.TotalSpace.proj β»ΒΉ' s)
The preimage under the projection from the tangent bundle of a set with unique differential in the basis also has unique differential.