𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.21027
inst✝¹⁰ : Ring 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup E
inst✝² : TopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous fun x => ∑ k in Finset.range n, ↑(p k) fun x_1 => x
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.21027
inst✝¹⁰ : Ring 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup E
inst✝² : TopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous (partialSum p n)
unfold partialSum
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.21027
inst✝¹⁰ : Ring 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup E
inst✝² : TopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous fun x => ∑ k in Finset.range n, ↑(p k) fun x_1 => x
continuity