feat(algebra/big_operators/order): Bound on a product from a pointwise bound (#10190)
feat(algebra/big_operators/order): Bound on a product from a pointwise bound (#10190)

This proves `finset.le_prod_of_forall_le` which is the dual of `finset.prod_le_of_forall_le`.





leanprover-community/mathlib,leanprover-community/mathlib