Equitable functions

Stream: Is there code for X?

[Yaël Dillies]

Is there anything in mathlib already to say that a function on a set doesn't reach values that are too different? I want to define

/-- A set is equitable if no element value is more than one bigger than another. -/
def equitable_on [has_le β] [has_add β] [has_one β] (s : set α) (f : α → β) : Prop :=
  ∀ ⦃a₁ a₂⦄, a₁ ∈ s → a₂ ∈ s → f a₁ ≤ f a₂ + 1

but maybe something more general already exists.