Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 16:51 d3f5adb0

View on Github →

feat(combinatorics/simple_graph/regularity/equitabilise): Equitabilising a partition (#13222) Define the equitabilisation of a partition and a way to find an arbitrary equipartition of any size.

Estimated changes

Created src/combinatorics/simple_graph/regularity/equitabilise.lean

added theorem finpartition.card_eq_of_mem_parts_equitabilise

added theorem finpartition.card_filter_equitabilise_big

added theorem finpartition.card_filter_equitabilise_small

added theorem finpartition.card_parts_equitabilise

added theorem finpartition.card_parts_equitabilise_subset_le

added theorem finpartition.equitabilise_aux

added theorem finpartition.equitabilise_is_equipartition

added theorem finpartition.exists_equipartition_card_eq

Modified src/order/partition/finpartition.lean

added theorem finpartition.mem_avoid