Theorems · Definition · order theory

Set.EquitableOn

{α : Type u_1} → {β : Type u_2} → [LE β] → [Add β] → [One β] → Set α → (α → β) → Prop

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

Defined in

Mathlib.Data.Set.Equitable

Cited by

12 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

LEAddOne