mathlib3

17ff82d9 - feat(topology/instances/ennreal): `ennreal.to_nnreal` applied to a `tsum` (#16320)

feat(topology/instances/ennreal): `ennreal.to_nnreal` applied to a `tsum` (#16320) If a function is finite for all inputs, then `to_nnreal` applied to the sum is the sum of `to_nnreal` applied to the values.