Commit 2022-02-25 05:25 f2fdef6f

View on Github →

feat(order/partition/equipartition): Equipartitions (#12023) Define finpartition.is_equipartition, a predicate for saying that the parts of a finpartition of a finset are all the same size up to a difference of 1.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.subsingleton_of_subset_singleton

Modified src/data/set/equitable.lean

added theorem finset.equitable_on.le

added theorem finset.equitable_on.le_add_one

modified theorem finset.equitable_on_iff

modified theorem finset.equitable_on_iff_le_le_add_one

Created src/order/partition/equipartition.lean

added theorem finpartition.bot_is_equipartition

added theorem finpartition.indiscrete_is_equipartition

added theorem finpartition.is_equipartition.average_le_card_part

added theorem finpartition.is_equipartition.card_part_le_average_add_one

added def finpartition.is_equipartition

added theorem finpartition.is_equipartition_iff_card_parts_eq_average

added theorem finpartition.top_is_equipartition

added theorem set.subsingleton.is_equipartition

Modified src/order/partition/finpartition.lean

added theorem finpartition.parts_top_subset

added theorem finpartition.parts_top_subsingleton