le — Mathlib · SciLib

English

Let m be a natural number and L a finite list of natural numbers which is m-admissible. Then for every index k with 0 ≤ k < length(L), the k-th entry of L satisfies L[k] ≤ m + k.

Русский

Пусть m ∈ ℕ и L — конечный список1 натуральных чисел, который является m-допустимым. Тогда для каждого индекса k с 0 ≤ k < длина(L) имеем L[k] ≤ m + k.

LaTeX

$$$\\\\text{Let } m \in \\mathbb{N} \text{ and } L = (L_0, \\dots, L_{n-1}) \text{ with } \\text{IsAdmissible}(m, L). \\\\text{Then } \\forall i \ (0 \\le i < n):\\ L_i \\le m + i.$$$

Lean4

theorem le {L : List ℕ} (hL : IsAdmissible m L) : ∀ (k : ℕ), (h : k < L.length) → L[k] ≤ m + k :=
  hL.2

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