Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_map.has_sum_apply

Modification history

2023-02-11 09:22
src/topology/continuous_function/algebra.lean
feat(topology/continuous_function): lemmas on infinite sums of continuous functions (#18424) …
Added continuous_map.has_sum_applyView on Github →