Differentiability of models with corners and (extended) charts #
In this file, we analyse the differentiability of charts, models with corners and extended charts. We show that
- models with corners are differentiable
- charts are differentiable on their source
mdifferentiableOn_extChartAt:extChartAtis differentiable on its source
Suppose a partial homeomorphism e is differentiable. This file shows
PartialHomeomorph.MDifferentiable.mfderiv: its derivative is a continuous linear equivalencePartialHomeomorph.MDifferentiable.mfderiv_bijective: its derivative is bijective; there are also spelling with trivial kernel and full range
In particular, (extended) charts have bijective differential.
Tags #
charts, differentiable, bijective
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).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).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.
theorem
mfderiv_chartAt_eq_tangentCoordChange
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_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}
(hsrc : x ∈ (chartAt H y).source)
:
mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y x
Differentiable partial 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 partial 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_11}
[NontriviallyNormedField 𝕜]
{E : Type u_12}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_13}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_14}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{x : M}
{y : M}
(h : y ∈ (chartAt H x).source)
:
HasMFDerivAt I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) y (mfderiv I I (↑(chartAt H x)) y)
theorem
hasMFDerivWithinAt_extChartAt
{𝕜 : Type u_11}
[NontriviallyNormedField 𝕜]
{E : Type u_12}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_13}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_14}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{s : Set M}
{x : M}
{y : M}
(h : y ∈ (chartAt H x).source)
:
HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) s y (mfderiv I I (↑(chartAt H x)) y)
theorem
mdifferentiableAt_extChartAt
{𝕜 : Type u_11}
[NontriviallyNormedField 𝕜]
{E : Type u_12}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_13}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_14}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{x : M}
{y : M}
(h : y ∈ (chartAt H x).source)
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) y
theorem
mdifferentiableOn_extChartAt
{𝕜 : Type u_11}
[NontriviallyNormedField 𝕜]
{E : Type u_12}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_13}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_14}
[TopologicalSpace M]
[ChartedSpace H M]
[SmoothManifoldWithCorners I M]
{x : M}
:
MDifferentiableOn I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) (chartAt H x).source