Commit 2020-10-04 20:49 d13d21ba

View on Github →

feat(algebra/big_operators/order): bounding finite fibration cardinalities from below (#4396) Also including unrelated change finset.inter_eq_sdiff_sdiff.

Estimated changes

Modified src/algebra/big_operators/order.lean

added theorem finset.mul_card_image_le_card

added theorem finset.mul_card_image_le_card_of_maps_to

Modified src/data/finset/basic.lean

added theorem finset.inter_eq_sdiff_sdiff