Derivatives on pi-types.

theorem hasFDerivAt_update {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [Fintype ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : (i : ι) → E i) {i : ι} (y : E i) : HasFDerivAt (Function.update x i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y

theorem hasFDerivAt_single {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [Fintype ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {i : ι} (y : E i) : HasFDerivAt (Pi.single i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y

theorem fderiv_update {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [Fintype ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : (i : ι) → E i) {i : ι} (y : E i) : fderiv 𝕜 (Function.update x i) y = ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))

theorem fderiv_single {𝕜 : Type u_1} {ι : Type u_2} [DecidableEq ι] [Fintype ι] [NontriviallyNormedField 𝕜] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {i : ι} (y : E i) : fderiv 𝕜 (Pi.single i) y = ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))