mathlib

20a461f3 - feat(algebra/big_operators/order): The size of a finset of disjoint finsets is less than the size of its union (#11654)

feat(algebra/big_operators/order): The size of a finset of disjoint finsets is less than the size of its union (#11654) Prove `card_le_card_bUnion`, its corollary `card_le_card_bUnion_add_card_fiber` where we drop the nonemptiness condition in exchange of a `+` card of the fiber of `∅` on the RHS, and its useful special case `card_le_card_bUnion_add_one`.