# The derivative of a linear equivalence #

For detailed documentation of the Fréchet derivative, see the module docstring of `Analysis/Calculus/FDeriv/Basic.lean`.

This file contains the usual formulas (and existence assertions) for the derivative of continuous linear equivalences.

We also prove the usual formula for the derivative of the inverse function, assuming it exists. The inverse function theorem is in `Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean`.

### Differentiability of linear equivs, and invariance of differentiability #

source
theorem ContinuousLinearEquiv.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :
HasStrictFDerivAt (⇑iso) (↑iso) x
source
theorem ContinuousLinearEquiv.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃L[𝕜] F) :
HasFDerivWithinAt (⇑iso) (↑iso) s x
source
theorem ContinuousLinearEquiv.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :
HasFDerivAt (⇑iso) (↑iso) x
source
theorem ContinuousLinearEquiv.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :
DifferentiableAt 𝕜 (⇑iso) x
source
theorem ContinuousLinearEquiv.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃L[𝕜] F) :
DifferentiableWithinAt 𝕜 (⇑iso) s x
source
theorem ContinuousLinearEquiv.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :
fderiv 𝕜 (⇑iso) x = ↑iso
source
theorem ContinuousLinearEquiv.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃L[𝕜] F) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (⇑iso) s x = ↑iso
source
theorem ContinuousLinearEquiv.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (iso : E ≃L[𝕜] F) :
Differentiable 𝕜 ⇑iso
source
theorem ContinuousLinearEquiv.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (iso : E ≃L[𝕜] F) :
DifferentiableOn 𝕜 (⇑iso) s
source
theorem ContinuousLinearEquiv.comp_differentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} :
DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
source
theorem ContinuousLinearEquiv.comp_differentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} :
DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
source
theorem ContinuousLinearEquiv.comp_differentiableOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} :
DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s
source
theorem ContinuousLinearEquiv.comp_differentiable_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} :
Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f
source
theorem ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x ↔ HasFDerivWithinAt f f' s x
source
theorem ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :
HasStrictFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x ↔ HasStrictFDerivAt f f' x
source
theorem ContinuousLinearEquiv.comp_hasFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :
HasFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x ↔ HasFDerivAt f f' x
source
theorem ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm).comp f') s x
source
theorem ContinuousLinearEquiv.comp_hasFDerivAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] F} :
HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f ((↑iso.symm).comp f') x
source
theorem ContinuousLinearEquiv.comp_fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (⇑iso ∘ f) s x = (↑iso).comp (fderivWithin 𝕜 f s x)
source
theorem ContinuousLinearEquiv.comp_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} :
fderiv 𝕜 (⇑iso ∘ f) x = (↑iso).comp (fderiv 𝕜 f x)
source
theorem fderivWithin_continuousLinearEquiv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {x : E} {s : Set E} (L : G ≃L[𝕜] G') (f : E → F →L[𝕜] G) (hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun (x : E) => (↑L).comp (f x)) s x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderivWithin 𝕜 f s x)
source
theorem fderiv_continuousLinearEquiv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (L : G ≃L[𝕜] G') (f : E → F →L[𝕜] G) (x : E) :
fderiv 𝕜 (fun (x : E) => (↑L).comp (f x)) x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
source
theorem fderiv_continuousLinearEquiv_comp' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (L : G ≃L[𝕜] G') (f : E → F →L[𝕜] G) :
(fderiv 𝕜 fun (x : E) => (↑L).comp (f x)) = fun (x : E) => (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
source
theorem ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} :
DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x)
source
theorem ContinuousLinearEquiv.comp_right_differentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} :
DifferentiableAt 𝕜 (f ∘ ⇑iso) x ↔ DifferentiableAt 𝕜 f (iso x)
source
theorem ContinuousLinearEquiv.comp_right_differentiableOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} :
DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s
source
theorem ContinuousLinearEquiv.comp_right_differentiable_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} :
Differentiable 𝕜 (f ∘ ⇑iso) ↔ Differentiable 𝕜 f
source
theorem ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} {f' : F →L[𝕜] G} :
HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x)
source
theorem ContinuousLinearEquiv.comp_right_hasFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} {f' : F →L[𝕜] G} :
HasFDerivAt (f ∘ ⇑iso) (f'.comp ↑iso) x ↔ HasFDerivAt f f' (iso x)
source
theorem ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} {f' : E →L[𝕜] G} :
HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f'.comp ↑iso.symm) s (iso x)
source
theorem ContinuousLinearEquiv.comp_right_hasFDerivAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} {f' : E →L[𝕜] G} :
HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (f'.comp ↑iso.symm) (iso x)
source
theorem ContinuousLinearEquiv.comp_right_fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} (hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x) :
fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = (fderivWithin 𝕜 f s (iso x)).comp ↑iso
source
theorem ContinuousLinearEquiv.comp_right_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} :
fderiv 𝕜 (f ∘ ⇑iso) x = (fderiv 𝕜 f (iso x)).comp ↑iso

### Differentiability of linear isometry equivs, and invariance of differentiability #

source
theorem LinearIsometryEquiv.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
HasStrictFDerivAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x
source
theorem LinearIsometryEquiv.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) :
HasFDerivWithinAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) s x
source
theorem LinearIsometryEquiv.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
HasFDerivAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x
source
theorem LinearIsometryEquiv.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
DifferentiableAt 𝕜 (⇑iso) x
source
theorem LinearIsometryEquiv.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) :
DifferentiableWithinAt 𝕜 (⇑iso) s x
source
theorem LinearIsometryEquiv.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
fderiv 𝕜 (⇑iso) x = ↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
source
theorem LinearIsometryEquiv.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (⇑iso) s x = ↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
source
theorem LinearIsometryEquiv.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (iso : E ≃ₗᵢ[𝕜] F) :
Differentiable 𝕜 ⇑iso
source
theorem LinearIsometryEquiv.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) :
DifferentiableOn 𝕜 (⇑iso) s
source
theorem LinearIsometryEquiv.comp_differentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} :
DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
source
theorem LinearIsometryEquiv.comp_differentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} :
DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
source
theorem LinearIsometryEquiv.comp_differentiableOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} :
DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s
source
theorem LinearIsometryEquiv.comp_differentiable_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} :
Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f
source
theorem LinearIsometryEquiv.comp_hasFDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :
HasFDerivWithinAt (⇑iso ∘ f) ((↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') s x ↔ HasFDerivWithinAt f f' s x
source
theorem LinearIsometryEquiv.comp_hasStrictFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :
HasStrictFDerivAt (⇑iso ∘ f) ((↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') x ↔ HasStrictFDerivAt f f' x
source
theorem LinearIsometryEquiv.comp_hasFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :
HasFDerivAt (⇑iso ∘ f) ((↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') x ↔ HasFDerivAt f f' x
source
theorem LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑{ toLinearEquiv := iso.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') s x
source
theorem LinearIsometryEquiv.comp_hasFDerivAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] F} :
HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f ((↑{ toLinearEquiv := iso.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp f') x
source
theorem LinearIsometryEquiv.comp_fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (⇑iso ∘ f) s x = (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderivWithin 𝕜 f s x)
source
theorem LinearIsometryEquiv.comp_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} :
fderiv 𝕜 (⇑iso ∘ f) x = (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)
source
theorem LinearIsometryEquiv.comp_fderiv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} :
fderiv 𝕜 (⇑iso ∘ f) = fun (x : G) => (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)
source
theorem HasFDerivWithinAt.of_local_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {g : F → E} {f' : E ≃L[𝕜] F} {a : F} {t : Set F} (hg : Filter.Tendsto g (nhdsWithin a t) (nhdsWithin (g a) s)) (hf : HasFDerivWithinAt f (↑f') s (g a)) (ha : a ∈ t) (hfg : ∀ᶠ (y : F) in nhdsWithin a t, f (g y) = y) :
HasFDerivWithinAt g (↑f'.symm) t a

If `f (g y) = y` for `y` in a neighborhood of `a` within `t`, `g` maps a neighborhood of `a` within `t` to a neighborhood of `g a` within `s`, and `f` has an invertible derivative `f'` at `g a` within `s`, then `g` has the derivative `f'⁻¹` at `a` within `t`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

source
theorem HasStrictFDerivAt.of_local_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a) (hf : HasStrictFDerivAt f (↑f') (g a)) (hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :
HasStrictFDerivAt g (↑f'.symm) a

If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an invertible derivative `f'` at `g a` in the strict sense, then `g` has the derivative `f'⁻¹` at `a` in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

source
theorem HasFDerivAt.of_local_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a) (hf : HasFDerivAt f (↑f') (g a)) (hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :
HasFDerivAt g (↑f'.symm) a

If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an invertible derivative `f'` at `g a`, then `g` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

source
theorem OpenPartialHomeomorph.hasStrictFDerivAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasStrictFDerivAt (↑f) (↑f') (↑f.symm a)) :
HasStrictFDerivAt (↑f.symm) (↑f'.symm) a

If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an invertible derivative `f'` in the sense of strict differentiability at `f.symm a`, then `f.symm` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

source
theorem OpenPartialHomeomorph.hasFDerivAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasFDerivAt (↑f) (↑f') (↑f.symm a)) :
HasFDerivAt (↑f.symm) (↑f'.symm) a

If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an invertible derivative `f'` at `f.symm a`, then `f.symm` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

source
theorem HasFDerivWithinAt.eventually_ne {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} {c : F} (h : HasFDerivWithinAt f f' s x) (hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖) :
∀ᶠ (z : E) in nhdsWithin x (s \ {x}), f z ≠ c
source
theorem HasFDerivAt.eventually_ne {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {c : F} (h : HasFDerivAt f f' x) (hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖) :
∀ᶠ (z : E) in nhdsWithin x {x}ᶜ, f z ≠ c
source
theorem has_fderiv_at_filter_real_equiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {f' : E →L[ℝ] F} {x : E} {L : Filter E} :
Filter.Tendsto (fun (x' : E) => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (nhds 0) ↔ Filter.Tendsto (fun (x' : E) => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (nhds 0)
source
theorem HasFDerivAt.lim_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {f' : E →L[ℝ] F} {x : E} (hf : HasFDerivAt f f' x) (v : E) :
Filter.Tendsto (fun (c : ℝ) => c • (f (x + c⁻¹ • v) - f x)) Filter.atTop (nhds (f' v))
source
theorem HasFDerivWithinAt.mapsTo_tangent_cone {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivWithinAt f f' s x) :
Set.MapsTo (⇑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (f '' s) (f x))

The image of a tangent cone under the differential of a map is included in the tangent cone to the image.

source
theorem HasFDerivWithinAt.uniqueDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivWithinAt f f' s x) (hs : UniqueDiffWithinAt 𝕜 s x) (h' : DenseRange ⇑f') :
UniqueDiffWithinAt 𝕜 (f '' s) (f x)

If a set has the unique differentiability property at a point x, then the image of this set under a map with onto derivative has also the unique differentiability property at the image point.

source
theorem UniqueDiffOn.image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E → E →L[𝕜] F} (hs : UniqueDiffOn 𝕜 s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hd : ∀ x ∈ s, DenseRange ⇑(f' x)) :
UniqueDiffOn 𝕜 (f '' s)
source
theorem HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (e' : E ≃L[𝕜] F) (h : HasFDerivWithinAt f (↑e') s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
UniqueDiffWithinAt 𝕜 (f '' s) (f x)
source
theorem ContinuousLinearEquiv.uniqueDiffOn_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (e : E ≃L[𝕜] F) (h : UniqueDiffOn 𝕜 s) :
UniqueDiffOn 𝕜 (⇑e '' s)
source
@[simp]
theorem ContinuousLinearEquiv.uniqueDiffOn_image_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (e : E ≃L[𝕜] F) :
UniqueDiffOn 𝕜 (⇑e '' s) ↔ UniqueDiffOn 𝕜 s
source
@[simp]
theorem ContinuousLinearEquiv.uniqueDiffOn_preimage_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (e : F ≃L[𝕜] E) :
UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
source
theorem UniqueDiffWithinAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} (h : UniqueDiffWithinAt 𝕜 s x) {c : 𝕜} (hc : c ≠ 0) :
UniqueDiffWithinAt 𝕜 (c • s) (c • x)
source
theorem UniqueDiffWithinAt.smul_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {c : 𝕜} (hc : c ≠ 0) :
UniqueDiffWithinAt 𝕜 (c • s) (c • x) ↔ UniqueDiffWithinAt 𝕜 s x
source
theorem fderivWithin_const_smul_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} {R : Type u_4} [DivisionRing R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) (hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x
source
theorem hasFDerivWithinAt_comp_smul_smul_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E →L[𝕜] F} {x : E} {c : 𝕜} :
HasFDerivWithinAt (fun (x : E) => f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)
source
theorem hasFDerivWithinAt_comp_smul_iff_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E →L[𝕜] F} {x : E} {c : 𝕜} (hc : c ≠ 0) :
HasFDerivWithinAt (fun (x : E) => f (c • x)) f' s x ↔ HasFDerivWithinAt (c • f) f' (c • s) (c • x)
source
theorem fderivWithin_comp_smul_eq_fderivWithin_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (c : 𝕜) :
fderivWithin 𝕜 (fun (x : E) => f (c • x)) s x = fderivWithin 𝕜 (c • f) (c • s) (c • x)
source
theorem fderivWithin_comp_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (c : 𝕜) (hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun (x : E) => f (c • x)) s x = c • fderivWithin 𝕜 f (c • s) (c • x)
source
theorem fderiv_comp_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (c : 𝕜) :
fderiv 𝕜 (fun (x : E) => f (c • x)) x = c • fderiv 𝕜 f (c • x)