R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
p✝ : R[X]
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => sum p fun e a => ↑f a * x ^ e
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
p✝ : R[X]
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => eval₂ f x p
simp only [eval₂_eq_sum, Finsupp.sum]
no goals
R : Type u_2
S : Type u_1
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
p✝ : R[X]
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => sum p fun e a => ↑f a * x ^ e
exact continuous_finset_sum _ fun c _ => continuous_const.mul (continuous_pow _)