mathlib

ddbfecf5 - feat(topology/continuous_function): lemmas on infinite sums of continuous functions (#18424)

feat(topology/continuous_function): lemmas on infinite sums of continuous functions (#18424) A lemma (in three variants) about evaluating infinite sums of continuous functions at a point. Split off from #18392.