Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-14 23:14 49fd7195

View on Github →

feat(topology/algebra,geometry/manifold): continuity and smoothness of locally finite products of functions (#7128)

Estimated changes

added theorem smooth_finprod
added theorem smooth_finprod_cond
added theorem smooth_finset_prod'
added theorem smooth_finset_prod
modified theorem continuous.mul
modified theorem continuous.pow
modified theorem continuous_at.mul
added theorem continuous_finprod
modified theorem continuous_finset_prod
modified theorem continuous_list_prod
modified theorem continuous_multiset_prod
modified theorem continuous_on.mul
modified theorem continuous_within_at.mul
modified theorem filter.tendsto.mul
modified theorem tendsto_finset_prod
modified theorem tendsto_list_prod
modified theorem tendsto_multiset_prod