Commit 2023-02-08 08:15 fea8b0d5

View on Github →

feat: port Combinatorics.SimpleGraph.Regularity.Equitabilise (#2087)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/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_isEquipartition

added theorem Finpartition.exists_equipartition_card_eq