mathlib
931cd6d7 - feat(data/set/equitable): Equitable functions (#8509)

Commit
4 years ago
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
Author
Parents
Loading