order): Bound on a product from a pointwise bound (#10190)

Commit

4 years ago

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`.

Author

YaelDillies

Parents

be412c3d

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

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