# Basic properties of the manifold Fréchet derivative #

In this file, we show various properties of the manifold Fréchet derivative, mimicking the API for Fréchet derivatives.

• basic properties of unique differentiability sets
• various general lemmas about the manifold Fréchet derivative
• deducing differentiability from smoothness,
• deriving continuity from differentiability on manifolds,
• congruence lemmas for derivatives on manifolds
• composition lemmas and the chain rule

### Unique differentiability sets in manifolds #

theorem uniqueMDiffWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {x : M} :
UniqueMDiffWithinAt I Set.univ x
theorem uniqueMDiffWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {x : M} :
UniqueDiffWithinAt 𝕜 ((extChartAt I x).symm ⁻¹' s (extChartAt I x).target) ((extChartAt I x) x)
theorem UniqueMDiffWithinAt.mono_nhds {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {t : Set M} {x : M} (hs : ) (ht : ) :
theorem UniqueMDiffWithinAt.mono_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {t : Set M} {x : M} (hs : ) (ht : t ) :
theorem UniqueMDiffWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {s : Set M} {t : Set M} (h : ) (st : s t) :
theorem UniqueMDiffWithinAt.inter' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {s : Set M} {t : Set M} (hs : ) (ht : t ) :
theorem UniqueMDiffWithinAt.inter {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {s : Set M} {t : Set M} (hs : ) (ht : t nhds x) :
theorem IsOpen.uniqueMDiffWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {x : M} {s : Set M} (hs : ) (xs : x s) :
theorem UniqueMDiffOn.inter {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) :
theorem IsOpen.uniqueMDiffOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {s : Set M} (hs : ) :
theorem uniqueMDiffOn_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] :
UniqueMDiffOn I Set.univ
theorem UniqueMDiffWithinAt.eq {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} {f₁' : →L[𝕜] TangentSpace I' (f x)} (U : ) (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} {f₁' : →L[𝕜] TangentSpace I' (f x)} (U : ) (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {x : M} {y : M'} {s : Set M} {t : Set M'} (hs : ) (ht : ) :
UniqueMDiffWithinAt (I.prod I') (s ×ˢ t) (x, y)
theorem UniqueMDiffOn.prod {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {s : Set M} {t : Set M'} (hs : ) (ht : ) :
UniqueMDiffOn (I.prod 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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {x : M} :
MDifferentiableWithinAt I I' f s x DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target (extChartAt I x).symm ⁻¹' s) ((extChartAt I x) x)
theorem mdifferentiableWithinAt_iff_of_mem_source {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {x' : M} {y : M'} (hx : x' (chartAt H x).source) (hy : f x' (chartAt H' y).source) :
MDifferentiableWithinAt I I' f s x' DifferentiableWithinAt 𝕜 ((extChartAt I' y) f (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s ) ((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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (h : ¬MDifferentiableWithinAt I I' f s x) :
mfderivWithin I I' f s x = 0
theorem mfderiv_zero_of_not_mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] (h : ¬MDifferentiableAt I I' f x) :
mfderiv I I' f x = 0
theorem HasMFDerivWithinAt.mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') :
theorem HasMFDerivAt.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') :
@[simp]
theorem hasMFDerivWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {f' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {f₀' : →L[𝕜] TangentSpace I' (f x)} {f₁' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : t ) :
HasMFDerivWithinAt I I' f (s t) x f' HasMFDerivWithinAt I I' f s x f'
theorem hasMFDerivWithinAt_inter {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (ht : s ) :
HasMFDerivWithinAt I I' f t x f'
theorem HasMFDerivWithinAt.hasMFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) :
mfderivWithin I I' f s x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).symm ⁻¹' s ) ((extChartAt I x) x)
theorem MDifferentiableAt.hasMFDerivAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] (h : MDifferentiableAt I I' f x) :
HasMFDerivAt I I' f x (mfderiv I I' f x)
theorem MDifferentiableAt.mfderiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') :
mfderiv I I' f x = f'
theorem HasMFDerivWithinAt.mfderivWithin {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (hxs : ) :
mfderivWithin I I' f s x = f'
theorem MDifferentiable.mfderivWithin {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableAt I I' f x) (hxs : ) :
mfderivWithin I I' f s x = mfderiv I I' f x
theorem mfderivWithin_subset {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (st : s t) (hs : ) (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} (hst : s t) (h : MDifferentiableWithinAt I I' f t x) :
theorem mdifferentiableWithinAt_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} :
MDifferentiableWithinAt I I' f Set.univ x MDifferentiableAt I I' f x
theorem mdifferentiableWithinAt_inter {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} (ht : t nhds x) :
theorem mdifferentiableWithinAt_inter' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} (ht : t ) :
theorem MDifferentiableAt.mdifferentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} (h : MDifferentiableAt I I' f x) :
theorem MDifferentiableWithinAt.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} (h : MDifferentiableWithinAt I I' f s x) (hs : s nhds x) :
theorem MDifferentiableOn.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} (h : MDifferentiableOn I I' f s) (hx : s nhds x) :
theorem MDifferentiableOn.mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} (h : MDifferentiableOn I I' f t) (st : s t) :
theorem mdifferentiableOn_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} :
MDifferentiableOn I I' f Set.univ MDifferentiable I I' f
theorem MDifferentiable.mdifferentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} (h : MDifferentiable I I' f) :
theorem mdifferentiableOn_of_locally_mdifferentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} (h : xs, ∃ (u : Set M), x u MDifferentiableOn I I' f (s u)) :
@[simp]
theorem mfderivWithin_univ {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} [Is : ] [I's : ] :
mfderivWithin I I' f Set.univ = mfderiv I I' f
theorem mfderivWithin_inter {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (h : s nhds x) :
mfderivWithin I I' f s x = mfderiv I I' f x
theorem mfderivWithin_of_isOpen {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (hs : ) (hx : x s) :
mfderivWithin I I' f s x = mfderiv I I' f x
theorem mfderivWithin_eq_mfderiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (hs : ) (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {x' : M} {y : M'} (hx : x' (chartAt H x).source) (hy : f x' (chartAt H' y).source) :
MDifferentiableAt I I' f x' ContinuousAt f x' DifferentiableWithinAt 𝕜 ((extChartAt I' y) f (extChartAt I x).symm) (Set.range I) ((extChartAt I x) x')

### Deducing differentiability from smoothness #

theorem ContMDiffWithinAt.mdifferentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} {n : ℕ∞} (hf : ContMDiffWithinAt I I' n f s x) (hn : 1 n) :
theorem ContMDiffAt.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {n : ℕ∞} (hf : ContMDiffAt I I' n f x) (hn : 1 n) :
theorem ContMDiffOn.mdifferentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {n : ℕ∞} (hf : ContMDiffOn I I' n f s) (hn : 1 n) :
theorem ContMDiff.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {n : ℕ∞} (hf : ContMDiff I I' n f) (hn : 1 n) :
theorem SmoothWithinAt.mdifferentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} (hf : SmoothWithinAt I I' f s x) :
theorem SmoothAt.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} (hf : SmoothAt I I' f x) :
theorem SmoothOn.mdifferentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} (hf : SmoothOn I I' f s) :
theorem Smooth.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} (hf : Smooth I I' f) :
theorem Smooth.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} (hf : Smooth I I' f) :
theorem Smooth.mdifferentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} (hf : Smooth I I' f) :

### Deriving continuity from differentiability on manifolds #

theorem HasMFDerivWithinAt.continuousWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') :
theorem HasMFDerivAt.continuousAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') :
theorem MDifferentiableOn.continuousOn {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} (h : MDifferentiableOn I I' f s) :
theorem MDifferentiable.continuous {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} (h : MDifferentiable I I' f) :
theorem tangentMapWithin_subset {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} {t : Set M} [Is : ] [I's : ] {p : } (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} [Is : ] [I's : ] :
tangentMapWithin I I' f Set.univ = tangentMap I I' f
theorem tangentMapWithin_eq_tangentMap {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} [Is : ] [I's : ] {p : } (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {s : Set M} [Is : ] [I's : ] {p : } :
(tangentMapWithin I I' f s p).proj = f p.proj
@[simp]
theorem tangentMap_proj {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} [Is : ] [I's : ] {p : } :
(tangentMap I I' f p).proj = f p.proj
theorem MDifferentiableWithinAt.prod_mk {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {x : M} {s : Set M} {f : MM'} {g : MM''} (hf : MDifferentiableWithinAt I I' f s x) (hg : MDifferentiableWithinAt I I'' g s x) :
MDifferentiableWithinAt I (I'.prod I'') (fun (x : M) => (f x, g x)) s x
theorem MDifferentiableAt.prod_mk {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {x : M} {f : MM'} {g : MM''} (hf : MDifferentiableAt I I' f x) (hg : MDifferentiableAt I I'' g x) :
MDifferentiableAt I (I'.prod I'') (fun (x : M) => (f x, g x)) x
theorem MDifferentiableOn.prod_mk {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {s : Set M} {f : MM'} {g : MM''} (hf : MDifferentiableOn I I' f s) (hg : MDifferentiableOn I I'' g s) :
MDifferentiableOn I (I'.prod I'') (fun (x : M) => (f x, g x)) s
theorem MDifferentiable.prod_mk {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : MM''} (hf : MDifferentiable I I' f) (hg : MDifferentiable I I'' g) :
MDifferentiable I (I'.prod I'') fun (x : M) => (f x, g x)
theorem MDifferentiableWithinAt.prod_mk_space {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {x : M} {s : Set M} {f : ME'} {g : ME''} (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {x : M} {f : ME'} {g : ME''} (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {s : Set M} {f : ME'} {g : ME''} (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {f : ME'} {g : ME''} (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 HasMFDerivAt.congr_mfderiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} {f₁' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivAt I I' f x f') (h' : f' = f₁') :
HasMFDerivAt I I' f x f₁'
theorem HasMFDerivWithinAt.congr_mfderiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} {f₁' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (h' : f' = f₁') :
HasMFDerivWithinAt I I' f s x f₁'
theorem HasMFDerivWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
HasMFDerivWithinAt I I' f₁ s x f'
theorem HasMFDerivWithinAt.congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] {f' : →L[𝕜] TangentSpace I' (f x)} (h : HasMFDerivWithinAt I I' f s x f') (ht : xt, 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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} [Is : ] [I's : ] {f' : →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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
theorem Filter.EventuallyEq.mdifferentiableWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] (I : ) {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
theorem MDifferentiableWithinAt.congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (ht : xt, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t s) :
theorem MDifferentiableWithinAt.congr {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (ht : xs, f₁ x = f x) (hx : f₁ x = f x) :
theorem MDifferentiableOn.congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} {t : Set M} [Is : ] [I's : ] (h : MDifferentiableOn I I' f s) (h' : xt, f₁ x = f x) (h₁ : t s) :
MDifferentiableOn I I' f₁ t
theorem MDifferentiableAt.congr_of_eventuallyEq {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} [Is : ] [I's : ] (h : MDifferentiableAt I I' f x) (hL : f₁ =ᶠ[nhds x] f) :
MDifferentiableAt I I' f₁ x
theorem MDifferentiableWithinAt.mfderivWithin_congr_mono {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} {t : Set M} [Is : ] [I's : ] (h : MDifferentiableWithinAt I I' f s x) (hs : xt, f₁ x = f x) (hx : f₁ x = f x) (hxt : ) (h₁ : t s) :
mfderivWithin I I' f₁ t x = mfderivWithin I I' f s x
theorem Filter.EventuallyEq.mfderivWithin_eq {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (hs : ) (hL : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
mfderivWithin I I' f₁ s x = mfderivWithin I I' f s x
theorem mfderivWithin_congr {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} {s : Set M} [Is : ] [I's : ] (hs : ) (hL : xs, 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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {s : Set M} [Is : ] [I's : ] (h : xs, f x = f₁ x) (p : ) (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {f₁ : MM'} {x : M} [Is : ] [I's : ] (hL : f₁ =ᶠ[nhds x] f) :
mfderiv I I' f₁ x = mfderiv I I' f x
theorem mfderiv_congr_point {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {x' : M} (h : x = x') :
mfderiv I I' f x = mfderiv I I' f 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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {f : MM'} {x : M} [Is : ] [I's : ] {f' : MM'} (h : f = f') :
mfderiv I I' f x = mfderiv I I' f' x

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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {x : M} {s : Set M} {g : M'M''} (h : ) :
{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) ((extChartAt I x).symm ⁻¹' s )
theorem HasMFDerivWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} (x : M) {s : Set M} {g : M'M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] {f' : →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 (g'.comp f')
theorem HasMFDerivAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} (x : M) {g : M'M''} [Is : ] [I's : ] [I''s : ] {f' : →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 (g'.comp f')

The chain rule for manifolds.

theorem HasMFDerivAt.comp_hasMFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} (x : M) {s : Set M} {g : M'M''} [Is : ] [I's : ] [I''s : ] {f' : →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 (g'.comp f')
theorem MDifferentiableWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} (x : M) {s : Set M} {g : M'M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableWithinAt I' I'' g u (f x)) (hf : MDifferentiableWithinAt I I' f s x) (h : s f ⁻¹' u) :
theorem MDifferentiableAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} (x : M) {g : M'M''} [Is : ] [I's : ] [I''s : ] (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} (x : M) {s : Set M} {g : M'M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableWithinAt I' I'' g u (f x)) (hf : MDifferentiableWithinAt I I' f s x) (h : s f ⁻¹' u) (hxs : ) :
mfderivWithin I I'' (g f) s x = (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x)
theorem mfderiv_comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} (x : M) {g : M'M''} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x) :
mfderiv I I'' (g f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
theorem mfderiv_comp_of_eq {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : M'M''} [Is : ] [I's : ] [I''s : ] {x : M} {y : M'} (hg : MDifferentiableAt I' I'' g y) (hf : MDifferentiableAt I I' f x) (hy : f x = y) :
mfderiv I I'' (g f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
theorem MDifferentiableOn.comp {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {g : M'M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : M'M''} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) :
MDifferentiable I I'' (g f)
theorem tangentMapWithin_comp_at {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {s : Set M} {g : M'M''} {u : Set M'} [Is : ] [I's : ] [I''s : ] (p : ) (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : M'M''} [Is : ] [I's : ] [I''s : ] (p : ) (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} {E : Type u_2} [] {H : Type u_3} [] {I : } {M : Type u_4} [] [] {E' : Type u_5} [] [NormedSpace 𝕜 E'] {H' : Type u_6} [] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [] [ChartedSpace H' M'] {E'' : Type u_8} [] [NormedSpace 𝕜 E''] {H'' : Type u_9} [] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [] [ChartedSpace H'' M''] {f : MM'} {g : M'M''} [Is : ] [I's : ] [I''s : ] (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) :
tangentMap I I'' (g f) = tangentMap I' I'' g tangentMap I I' f