case h
α : Type u_1
β : Type ?u.60538
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀✝ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
x₀ : E
hf0 : Summable fun n => f n x₀
x : E
⊢ fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x
α : Type u_1
β : Type ?u.60538
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀✝ x : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
x₀ : E
hf0 : Summable fun n => f n x₀
⊢ (fderiv 𝕜 fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), fderiv 𝕜 (f n) x
ext1 x
no goals
case h
α : Type u_1
β : Type ?u.60538
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
v : ℕ → α → ℝ
s : Set E
x₀✝ x✝ : E
N : ℕ∞
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
x₀ : E
hf0 : Summable fun n => f n x₀
x : E
⊢ fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x
exact fderiv_tsum_apply hu hf hf' hf0 x