IsAdmissible — Mathlib

English

A list L of natural numbers is m-admissible if it is strictly increasing and each term L_k satisfies L_k ≤ m + k.

Русский

Порядокированный по возрастанию список натуральных чисел L называется m-приемлемым, если каждая компонента удовлетворяет L_k ≤ m + k.

LaTeX

$$IsAdmissible(m, L) := List.Sorted((<)) L ∧ ∀ k, k < |L| → L[k] ≤ m + k$$

Lean4

/-- A list of natural numbers [i₀, ⋯, iₙ]) is said to be `m`-admissible (for `m : ℕ`) if
`i₀ < ⋯ < iₙ` and `iₖ ≤ m + k` for all `k`.
-/
def IsAdmissible (L : List ℕ) : Prop :=
  List.Sorted (· < ·) L ∧ ∀ (k : ℕ), (h : k < L.length) → L[k] ≤ m + k

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