Theorem hasProd_of_isGLB_of_le_one

Modification history

2025-12-01 19:09
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
feat(Topology/Order): `HasProd` and `tprod` lemmas for ENNReal (#32276) …
Added hasProd_of_isGLB_of_le_oneView on Github →