mathlib3

7c94fe71 - feat(combinatorics/simple_graph/density): Bound on the difference between edge densities (#15353)

feat(combinatorics/simple_graph/density): Bound on the difference between edge densities (#15353) Auxiliary lemma for Szemerédi Regularity Lemma. Co-authored-by: Bhavik Mehta <bhavik@mehta8@gmail.com>