length_eraseIdx_add_one — Mathlib

English

Removing the i-th element keeps the length decrease by exactly 1: |l.eraseIdx i| = |l| - 1 for i < |l|.

Русский

Удаление i-го элемента уменьшает длину списка на ровно 1: |l.eraseIdx i| = |l| - 1 при i < |l|.

LaTeX

$$$ \\forall l,i\\ (i < l.\\text{length}):\\ |l.\\text{eraseIdx } i| + 1 = |l| $$$

Lean4

theorem length_eraseIdx_add_one {l : List ι} {i : ℕ} (h : i < l.length) : (l.eraseIdx i).length + 1 = l.length := by
  grind

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