Commit 2025-12-01 19:09 c8807004

feat(Topology/Order): HasProd and tprod lemmas for ENNReal (#32276) Add a few related missing lemmas with the main goal to prove that the product of a sequence of ENNReals between 0 and 1 converges and give a formula in terms of the infimum on Finsets. This is useful in probability (which is why it was proved for ENNReal in particular).