tail — Mathlib

English

If a :: L is m-admissible, then the tail L is (m+1)-admissible.

Русский

Если список вида a :: L является m-допустимым, то хвост L является (m+1)-допустимым.

LaTeX

$$$\\\\text{If } a :: L \\\\text{ is } m\\text{-admissible, then } L \\\\text{ is } (m+1)\\text{-admissible.}$$$

Lean4

/-- The tail of an `m`-admissible list is (m+1)-admissible. -/
theorem tail (a : ℕ) (l : List ℕ) (h : IsAdmissible m (a :: l)) : IsAdmissible (m + 1) l :=
  by
  refine ⟨(List.sorted_cons.mp h.sorted).right, ?_⟩
  intro k _
  simpa [Nat.add_assoc, Nat.add_comm 1] using h.le (k + 1) (by simpa)

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