Equitable functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines equitable functions.
f is equitable on a set
f a₁ ≤ f a₂ + 1 for all
a₁, a₂ ∈ s. This is mostly
useful when the codomain of
ℤ (or more generally a successor order).
ℕ can be replaced by any
conditionally_complete_monoid, but we don't have the
A set is equitable if no element value is more than one bigger than another.