Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 22:39 931cd6d7

View on Github →

feat(data/set/equitable): Equitable functions (#8509) Equitable functions are functions whose maximum is at most one more than their minimum. Equivalently, in an additive successor order (a < b ↔ a +1 ≤ b), this means that the function takes only values a and a + 1 for some a. From Szemerédi's regularity lemma. Co-authored by @b-mehta

Estimated changes