continuous.sum

Stream: Is there code for X?

[Johan Commelin]

continuous.add shows that the sum of two continuous maps is ctu. I can't find the analogue for a family of ctu maps in mathlib? Is this missing, or am I blind?

[Hanting Zhang]

Hmm, it's weirdly named, but does this work? docs#continuous_finset_sum

[Johan Commelin]

Thanks, that looks good!

[Patrick Massot]

Why do you say this is weird name?

[Johan Commelin]

I understand that you can't use dot notation in this case.

[Johan Commelin]

But there's a bit of a pattern between continuous_add and continuous.add.

[Johan Commelin]

So continuous_(finset_)sum would be continuity of the summation map A ^ n -> A. And continuous.(finset_)sum would be for sums of maps.

[Hanting Zhang]

Patrick Massot said:

Why do you say this is weird name?

In my experience the convention is X_add generalizes to X_sum, where the sum is implied to be over a finset.

[Hanting Zhang]

I think it would make sense to me if there was another continuous_sum about something more frequently used than finset sums, but there isn't. :thinking: