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 succ_order
+ conditionally_complete_monoid
, but we don't have the
latter yet.
@[simp]
theorem
set.equitable_on_empty
{α : Type u_1}
{β : Type u_2}
[has_le β]
[has_add β]
[has_one β]
(f : α → β) :
theorem
set.subsingleton.equitable_on
{α : Type u_1}
{β : Type u_2}
[ordered_semiring β]
{s : set α}
(hs : s.subsingleton)
(f : α → β) :
s.equitable_on f
theorem
set.equitable_on_singleton
{α : Type u_1}
{β : Type u_2}
[ordered_semiring β]
(a : α)
(f : α → β) :
{a}.equitable_on f