drop_take_succ_eq_cons_getElem — Mathlib

English

For any list L and i with i < length L, (L.take (i+1)).drop i equals the singleton [L[i]].

Русский

Для списка L и i с i < длина(L) получаем: (L.take (i+1)).drop i = [L[i]].

LaTeX

$$$$ \\text{If } i < |L|, \\ (L.take(i+1)).drop i = [L[i]]. $$$$

Lean4

/-- Taking only the first `i+1` elements in a list, and then dropping the first `i` ones, one is
left with a list of length `1` made of the `i`-th element of the original list. -/
theorem drop_take_succ_eq_cons_getElem (L : List α) (i : Nat) (h : i < L.length) : (L.take (i + 1)).drop i = [L[i]] :=
  by induction L generalizing i with grind

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