continuity of sums

Stream: Is there code for X?

[Adam Topaz]

I'm looking for a lemma that says the following: Given a topological space $X$ and a finite collection of continuous maps $f_i : X \to \mathbb{R}$, the (pointwise) sum $\sum_i f_i$ is continuous. I looked around has_continuous_add, but didn't find it. Am I looking in the wrong place (or am I just blind)?

[Eric Rodriguez]

docs#continuous_finset_sum? I found the finsum version first, which is weird...

[Adam Topaz]

Perfect thanks!