EquitableOn — Mathlib

English

EquitableOn(s,f) holds when for all a1,a2 in s, f(a1) ≤ f(a2) + 1.

Русский

EquitableOn(s,f) означает, что для всех a1,a2 в s выполняется f(a1) ≤ f(a2) + 1.

LaTeX

$$$\mathrm{EquitableOn}(s,f) \iff \forall a_1,a_2 \in s,\ f(a_1) \le f(a_2) + 1$$$

Lean4

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

Похожие утверждения