Commit 2023-02-11 09:22 ddbfecf5

View on Github →

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.

Estimated changes

Modified src/topology/continuous_function/algebra.lean

modified def continuous_map.coe_fn_monoid_hom

modified theorem continuous_map.coe_prod

modified def continuous_map.comp_monoid_hom'

added theorem continuous_map.has_sum_apply

modified theorem continuous_map.prod_apply

added theorem continuous_map.summable_apply

added theorem continuous_map.tsum_apply