Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-23 17:29 f458eef3

View on Github →

feat(analysis/topology): add tendsto and continuity rules for big operators

Estimated changes

Modified analysis/measure_theory/borel_space.lean

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_structures.lean

modified theorem continuous_add'

modified theorem continuous_add

added theorem continuous_finset_prod

added theorem continuous_finset_sum

added theorem continuous_list_prod

added theorem continuous_list_sum

added theorem continuous_mul'

modified theorem continuous_mul

added theorem continuous_multiset_prod

added theorem continuous_multiset_sum

modified theorem tendsto_add'

modified theorem tendsto_add

added theorem tendsto_finset_prod

added theorem tendsto_finset_sum

added theorem tendsto_list_prod

added theorem tendsto_list_sum

added theorem tendsto_mul'

modified theorem tendsto_mul

added theorem tendsto_multiset_prod

added theorem tendsto_multiset_sum

deleted theorem tendsto_sum