Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-14 04:42 6550cbac

View on Github →

feat(order/partition/finpartition): Finite partitions (#9795) This defines finite partitions along with quite a few constructions,

Estimated changes

modified theorem finset.disjoint_sup_left
modified theorem finset.disjoint_sup_right
modified theorem finset.inf_sup_distrib_left
modified theorem finset.sup_inf_distrib_left
added theorem finset.mk_mem_product
added theorem finpartition.card_bind
added theorem finpartition.card_bot
added theorem finpartition.card_mono
added theorem finpartition.mem_bind
added theorem finpartition.ne_bot
added theorem finpartition.parts_bot
added theorem finpartition.parts_inf
added structure finpartition