Derivative of the cartesian product of functions

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 cartesian products of functions, and functions into Pi-types.

Derivative of the cartesian product of two functions

theorem HasStrictFDerivAt.prod {𝕜 : 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] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasStrictFDerivAt f₁ f₁' x) (hf₂ : HasStrictFDerivAt f₂ f₂' x) : HasStrictFDerivAt (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') x

theorem HasFDerivAtFilter.prod {𝕜 : 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] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {L : Filter E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasFDerivAtFilter f₁ f₁' x L) (hf₂ : HasFDerivAtFilter f₂ f₂' x L) : HasFDerivAtFilter (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') x L

theorem HasFDerivWithinAt.prod {𝕜 : 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] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {s : Set E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasFDerivWithinAt f₁ f₁' s x) (hf₂ : HasFDerivWithinAt f₂ f₂' s x) : HasFDerivWithinAt (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') s x

theorem HasFDerivAt.prod {𝕜 : 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] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasFDerivAt f₁ f₁' x) (hf₂ : HasFDerivAt f₂ f₂' x) : HasFDerivAt (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') x

theorem hasFDerivAt_prod_mk_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e₀ : E) (f₀ : F) : HasFDerivAt (fun (e : E) => (e, f₀)) (ContinuousLinearMap.inl 𝕜 E F) e₀

theorem hasFDerivAt_prod_mk_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e₀ : E) (f₀ : F) : HasFDerivAt (fun (f : F) => (e₀, f)) (ContinuousLinearMap.inr 𝕜 E F) f₀

theorem DifferentiableWithinAt.prod {𝕜 : 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] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G} (hf₁ : DifferentiableWithinAt 𝕜 f₁ s x) (hf₂ : DifferentiableWithinAt 𝕜 f₂ s x) : DifferentiableWithinAt 𝕜 (fun (x : E) => (f₁ x, f₂ x)) s x

@[simp]

theorem DifferentiableAt.prod {𝕜 : 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] {f₁ : E → F} {x : E} {f₂ : E → G} (hf₁ : DifferentiableAt 𝕜 f₁ x) (hf₂ : DifferentiableAt 𝕜 f₂ x) : DifferentiableAt 𝕜 (fun (x : E) => (f₁ x, f₂ x)) x

theorem DifferentiableOn.prod {𝕜 : 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] {f₁ : E → F} {s : Set E} {f₂ : E → G} (hf₁ : DifferentiableOn 𝕜 f₁ s) (hf₂ : DifferentiableOn 𝕜 f₂ s) : DifferentiableOn 𝕜 (fun (x : E) => (f₁ x, f₂ x)) s

@[simp]

theorem Differentiable.prod {𝕜 : 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] {f₁ : E → F} {f₂ : E → G} (hf₁ : Differentiable 𝕜 f₁) (hf₂ : Differentiable 𝕜 f₂) : Differentiable 𝕜 fun (x : E) => (f₁ x, f₂ x)

theorem DifferentiableAt.fderiv_prod {𝕜 : 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] {f₁ : E → F} {x : E} {f₂ : E → G} (hf₁ : DifferentiableAt 𝕜 f₁ x) (hf₂ : DifferentiableAt 𝕜 f₂ x) : fderiv 𝕜 (fun (x : E) => (f₁ x, f₂ x)) x = ContinuousLinearMap.prod (fderiv 𝕜 f₁ x) (fderiv 𝕜 f₂ x)

theorem DifferentiableWithinAt.fderivWithin_prod {𝕜 : 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] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G} (hf₁ : DifferentiableWithinAt 𝕜 f₁ s x) (hf₂ : DifferentiableWithinAt 𝕜 f₂ s x) (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun (x : E) => (f₁ x, f₂ x)) s x = ContinuousLinearMap.prod (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f₂ s x)

theorem hasStrictFDerivAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : HasStrictFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p

theorem HasStrictFDerivAt.fst {𝕜 : 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] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasStrictFDerivAt f₂ f₂' x) : HasStrictFDerivAt (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') x

theorem hasFDerivAtFilter_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {L : Filter (E × F)} : HasFDerivAtFilter Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p L

theorem HasFDerivAtFilter.fst {𝕜 : 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] {x : E} {L : Filter E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAtFilter f₂ f₂' x L) : HasFDerivAtFilter (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') x L

theorem hasFDerivAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : HasFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p

theorem HasFDerivAt.fst {𝕜 : 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] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAt f₂ f₂' x) : HasFDerivAt (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') x

theorem hasFDerivWithinAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} : HasFDerivWithinAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) s p

theorem HasFDerivWithinAt.fst {𝕜 : 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] {x : E} {s : Set E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivWithinAt f₂ f₂' s x) : HasFDerivWithinAt (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') s x

theorem differentiableAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : DifferentiableAt 𝕜 Prod.fst p

@[simp]

theorem DifferentiableAt.fst {𝕜 : 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] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) : DifferentiableAt 𝕜 (fun (x : E) => (f₂ x).1) x

theorem differentiable_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] : Differentiable 𝕜 Prod.fst

@[simp]

theorem Differentiable.fst {𝕜 : 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] {f₂ : E → F × G} (h : Differentiable 𝕜 f₂) : Differentiable 𝕜 fun (x : E) => (f₂ x).1

theorem differentiableWithinAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} : DifferentiableWithinAt 𝕜 Prod.fst s p

theorem DifferentiableWithinAt.fst {𝕜 : 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] {x : E} {s : Set E} {f₂ : E → F × G} (h : DifferentiableWithinAt 𝕜 f₂ s x) : DifferentiableWithinAt 𝕜 (fun (x : E) => (f₂ x).1) s x

theorem differentiableOn_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set (E × F)} : DifferentiableOn 𝕜 Prod.fst s

theorem DifferentiableOn.fst {𝕜 : 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] {s : Set E} {f₂ : E → F × G} (h : DifferentiableOn 𝕜 f₂ s) : DifferentiableOn 𝕜 (fun (x : E) => (f₂ x).1) s

theorem fderiv_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : fderiv 𝕜 Prod.fst p = ContinuousLinearMap.fst 𝕜 E F

theorem fderiv.fst {𝕜 : 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] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) : fderiv 𝕜 (fun (x : E) => (f₂ x).1) x = ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) (fderiv 𝕜 f₂ x)

theorem fderivWithin_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} (hs : UniqueDiffWithinAt 𝕜 s p) : fderivWithin 𝕜 Prod.fst s p = ContinuousLinearMap.fst 𝕜 E F

theorem fderivWithin.fst {𝕜 : 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] {x : E} {s : Set E} {f₂ : E → F × G} (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f₂ s x) : fderivWithin 𝕜 (fun (x : E) => (f₂ x).1) s x = ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) (fderivWithin 𝕜 f₂ s x)

theorem hasStrictFDerivAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : HasStrictFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p

theorem HasStrictFDerivAt.snd {𝕜 : 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] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasStrictFDerivAt f₂ f₂' x) : HasStrictFDerivAt (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') x

theorem hasFDerivAtFilter_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {L : Filter (E × F)} : HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p L

theorem HasFDerivAtFilter.snd {𝕜 : 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] {x : E} {L : Filter E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAtFilter f₂ f₂' x L) : HasFDerivAtFilter (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') x L

theorem hasFDerivAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : HasFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p

theorem HasFDerivAt.snd {𝕜 : 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] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAt f₂ f₂' x) : HasFDerivAt (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') x

theorem hasFDerivWithinAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} : HasFDerivWithinAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) s p

theorem HasFDerivWithinAt.snd {𝕜 : 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] {x : E} {s : Set E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivWithinAt f₂ f₂' s x) : HasFDerivWithinAt (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') s x

theorem differentiableAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : DifferentiableAt 𝕜 Prod.snd p

@[simp]

theorem DifferentiableAt.snd {𝕜 : 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] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) : DifferentiableAt 𝕜 (fun (x : E) => (f₂ x).2) x

theorem differentiable_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] : Differentiable 𝕜 Prod.snd

@[simp]

theorem Differentiable.snd {𝕜 : 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] {f₂ : E → F × G} (h : Differentiable 𝕜 f₂) : Differentiable 𝕜 fun (x : E) => (f₂ x).2

theorem differentiableWithinAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} : DifferentiableWithinAt 𝕜 Prod.snd s p

theorem DifferentiableWithinAt.snd {𝕜 : 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] {x : E} {s : Set E} {f₂ : E → F × G} (h : DifferentiableWithinAt 𝕜 f₂ s x) : DifferentiableWithinAt 𝕜 (fun (x : E) => (f₂ x).2) s x

theorem differentiableOn_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set (E × F)} : DifferentiableOn 𝕜 Prod.snd s

theorem DifferentiableOn.snd {𝕜 : 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] {s : Set E} {f₂ : E → F × G} (h : DifferentiableOn 𝕜 f₂ s) : DifferentiableOn 𝕜 (fun (x : E) => (f₂ x).2) s

theorem fderiv_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} : fderiv 𝕜 Prod.snd p = ContinuousLinearMap.snd 𝕜 E F

theorem fderiv.snd {𝕜 : 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] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) : fderiv 𝕜 (fun (x : E) => (f₂ x).2) x = ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) (fderiv 𝕜 f₂ x)

theorem fderivWithin_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} (hs : UniqueDiffWithinAt 𝕜 s p) : fderivWithin 𝕜 Prod.snd s p = ContinuousLinearMap.snd 𝕜 E F

theorem fderivWithin.snd {𝕜 : 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] {x : E} {s : Set E} {f₂ : E → F × G} (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f₂ s x) : fderivWithin 𝕜 (fun (x : E) => (f₂ x).2) s x = ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) (fderivWithin 𝕜 f₂ s x)

theorem HasStrictFDerivAt.prodMap {𝕜 : 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'] {f : E → F} {f' : E →L[𝕜] F} {f₂ : G → G'} {f₂' : G →L[𝕜] G'} (p : E × G) (hf : HasStrictFDerivAt f f' p.1) (hf₂ : HasStrictFDerivAt f₂ f₂' p.2) : HasStrictFDerivAt (Prod.map f f₂) (ContinuousLinearMap.prodMap f' f₂') p

theorem HasFDerivAt.prodMap {𝕜 : 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'] {f : E → F} {f' : E →L[𝕜] F} {f₂ : G → G'} {f₂' : G →L[𝕜] G'} (p : E × G) (hf : HasFDerivAt f f' p.1) (hf₂ : HasFDerivAt f₂ f₂' p.2) : HasFDerivAt (Prod.map f f₂) (ContinuousLinearMap.prodMap f' f₂') p

@[simp]

theorem DifferentiableAt.prod_map {𝕜 : 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'] {f : E → F} {f₂ : G → G'} (p : E × G) (hf : DifferentiableAt 𝕜 f p.1) (hf₂ : DifferentiableAt 𝕜 f₂ p.2) : DifferentiableAt 𝕜 (fun (p : E × G) => (f p.1, f₂ p.2)) p

Derivatives of functions f : E → Π i, F' i

In this section we formulate has*FDeriv*_pi theorems as iffs, and provide two versions of each theorem:

• the version without ' deals with φ : Π i, E → F' i and φ' : Π i, E →L[𝕜] F' i and is designed to deduce differentiability of fun x i ↦ φ i x from differentiability of each φ i;
• the version with ' deals with Φ : E → Π i, F' i and Φ' : E →L[𝕜] Π i, F' i and is designed to deduce differentiability of the components fun x ↦ Φ x i from differentiability of Φ.

@[simp]

theorem hasStrictFDerivAt_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} : HasStrictFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x

theorem hasStrictFDerivAt_pi'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} (hφ : ∀ (i : ι), HasStrictFDerivAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x) : HasStrictFDerivAt Φ Φ' x

theorem hasStrictFDerivAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) : HasStrictFDerivAt (fun (f : (i : ι) → F' i) => f i) (ContinuousLinearMap.proj i) f

@[simp]

theorem hasStrictFDerivAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} : HasStrictFDerivAt (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasStrictFDerivAt (φ i) (φ' i) x

@[simp]

theorem hasFDerivAtFilter_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {L : Filter E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} : HasFDerivAtFilter Φ Φ' x L ↔ ∀ (i : ι), HasFDerivAtFilter (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x L

theorem hasFDerivAtFilter_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {L : Filter E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} : HasFDerivAtFilter (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') x L ↔ ∀ (i : ι), HasFDerivAtFilter (φ i) (φ' i) x L

@[simp]

theorem hasFDerivAt_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} : HasFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasFDerivAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x

theorem hasFDerivAt_pi'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} (hφ : ∀ (i : ι), HasFDerivAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x) : HasFDerivAt Φ Φ' x

theorem hasFDerivAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) : HasFDerivAt (fun (f : (i : ι) → F' i) => f i) (ContinuousLinearMap.proj i) f

theorem hasFDerivAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} : HasFDerivAt (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasFDerivAt (φ i) (φ' i) x

@[simp]

theorem hasFDerivWithinAt_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} : HasFDerivWithinAt Φ Φ' s x ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') s x

theorem hasFDerivWithinAt_pi'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} (hφ : ∀ (i : ι), HasFDerivWithinAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') s x) : HasFDerivWithinAt Φ Φ' s x

theorem hasFDerivWithinAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) (s' : Set ((i : ι) → F' i)) : HasFDerivWithinAt (fun (f : (i : ι) → F' i) => f i) (ContinuousLinearMap.proj i) s' f

theorem hasFDerivWithinAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} : HasFDerivWithinAt (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') s x ↔ ∀ (i : ι), HasFDerivWithinAt (φ i) (φ' i) s x

@[simp]

theorem differentiableWithinAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : DifferentiableWithinAt 𝕜 Φ s x ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun (x : E) => Φ x i) s x

theorem differentiableWithinAt_pi'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} (hφ : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun (x : E) => Φ x i) s x) : DifferentiableWithinAt 𝕜 Φ s x

theorem differentiableWithinAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) (s' : Set ((i : ι) → F' i)) : DifferentiableWithinAt 𝕜 (fun (f : (i : ι) → F' i) => f i) s' f

@[simp]

theorem differentiableAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : DifferentiableAt 𝕜 Φ x ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun (x : E) => Φ x i) x

theorem differentiableAt_pi'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} (hφ : ∀ (i : ι), DifferentiableAt 𝕜 (fun (x : E) => Φ x i) x) : DifferentiableAt 𝕜 Φ x

theorem differentiableAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) : DifferentiableAt 𝕜 (fun (f : (i : ι) → F' i) => f i) f

theorem differentiableOn_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : DifferentiableOn 𝕜 Φ s ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun (x : E) => Φ x i) s

theorem differentiableOn_pi'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} (hφ : ∀ (i : ι), DifferentiableOn 𝕜 (fun (x : E) => Φ x i) s) : DifferentiableOn 𝕜 Φ s

theorem differentiableOn_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (s' : Set ((i : ι) → F' i)) : DifferentiableOn 𝕜 (fun (f : (i : ι) → F' i) => f i) s'

theorem differentiable_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} : Differentiable 𝕜 Φ ↔ ∀ (i : ι), Differentiable 𝕜 fun (x : E) => Φ x i

theorem differentiable_pi'' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} (hφ : ∀ (i : ι), Differentiable 𝕜 fun (x : E) => Φ x i) : Differentiable 𝕜 Φ

theorem differentiable_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) : Differentiable 𝕜 fun (f : (i : ι) → F' i) => f i

theorem fderivWithin_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} (h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (φ i) s x) (hs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun (x : E) (i : ι) => φ i x) s x = ContinuousLinearMap.pi fun (i : ι) => fderivWithin 𝕜 (φ i) s x

theorem fderiv_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} (h : ∀ (i : ι), DifferentiableAt 𝕜 (φ i) x) : fderiv 𝕜 (fun (x : E) (i : ι) => φ i x) x = ContinuousLinearMap.pi fun (i : ι) => fderiv 𝕜 (φ i) x