# Equitable functions #

This file defines equitable functions.

A function f is equitable on a set s if f a₁ ≤ f a₂ + 1 for all a₁, a₂ ∈ s. This is mostly useful when the codomain of f is ℕ or ℤ (or more generally a successor order).

## TODO #

ℕ can be replaced by any SuccOrder + ConditionallyCompleteMonoid, but we don't have the latter yet.

def Set.EquitableOn {α : Type u_1} {β : Type u_2} [LE β] [Add β] [One β] (s : Set α) (f : αβ) :

A set is equitable if no element value is more than one bigger than another.

Equations
• s.EquitableOn f = ∀ ⦃a₁ a₂ : α⦄, a₁ sa₂ sf a₁ f a₂ + 1
Instances For
@[simp]
theorem Set.equitableOn_empty {α : Type u_1} {β : Type u_2} [LE β] [Add β] [One β] (f : αβ) :
.EquitableOn f
theorem Set.equitableOn_iff_exists_le_le_add_one {α : Type u_1} {s : Set α} {f : α} :
s.EquitableOn f ∃ (b : ), as, b f a f a b + 1
theorem Set.equitableOn_iff_exists_image_subset_icc {α : Type u_1} {s : Set α} {f : α} :
s.EquitableOn f ∃ (b : ), f '' s Set.Icc b (b + 1)
theorem Set.equitableOn_iff_exists_eq_eq_add_one {α : Type u_1} {s : Set α} {f : α} :
s.EquitableOn f ∃ (b : ), as, f a = b f a = b + 1
@[simp]
theorem Set.not_equitableOn {α : Type u_1} {β : Type u_2} [] [Add β] [One β] {s : Set α} {f : αβ} :
¬s.EquitableOn f as, bs, f b + 1 < f a
theorem Set.Subsingleton.equitableOn {α : Type u_1} {β : Type u_2} [] {s : Set α} (hs : s.Subsingleton) (f : αβ) :
s.EquitableOn f
theorem Set.equitableOn_singleton {α : Type u_1} {β : Type u_2} [] (a : α) (f : αβ) :
{a}.EquitableOn f
theorem Finset.equitableOn_iff_le_le_add_one {α : Type u_1} {s : } {f : α} :
(s).EquitableOn f as, (is, f i) / s.card f a f a (is, f i) / s.card + 1
theorem Finset.EquitableOn.le {α : Type u_1} {s : } {f : α} {a : α} (h : (s).EquitableOn f) (ha : a s) :
(is, f i) / s.card f a
theorem Finset.EquitableOn.le_add_one {α : Type u_1} {s : } {f : α} {a : α} (h : (s).EquitableOn f) (ha : a s) :
f a (is, f i) / s.card + 1
theorem Finset.equitableOn_iff {α : Type u_1} {s : } {f : α} :
(s).EquitableOn f as, f a = (is, f i) / s.card f a = (is, f i) / s.card + 1