ext
case empty
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x = ∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x
case empty.H
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝¹ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffOn 𝕜 (↑i) (f j) s
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun x => ∑ j in ∅, f j x) s x) x✝ = (∑ j in ∅, iteratedFDerivWithin 𝕜 i (f j) s x) x✝