mathlib

f51de876 - feat(combinatorics/simple_graph/regularity/chunk): Partition of a part (#18371)

feat(combinatorics/simple_graph/regularity/chunk): Partition of a part (#18371) The heart of the calculation of Szemerédi Regularity Lemma. Define the partition of a part of the original partition and show it locally increases the energy. This is all internal to the proof of SRL, so I made most lemmas `private`