Commit 2021-11-06 18:49 ebe7951d

View on Github →

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.

Estimated changes

Modified src/algebra/big_operators/order.lean

modified theorem finset.card_bUnion_le_card_mul

added theorem finset.le_prod_of_forall_le

modified theorem finset.prod_le_of_forall_le