take_one_drop_eq_of_lt_length — Mathlib

English

If n is less than the length of l, then the first element of the tail after dropping n is exactly the element at position n.

Русский

Если n < длина(l), то первый элемент после отброса n позиций равен l[n].

LaTeX

$$$ (l.drop\ n).take\ 1 = [l[n]] $$$

Lean4

theorem take_one_drop_eq_of_lt_length {l : List α} {n : ℕ} (h : n < l.length) : (l.drop n).take 1 = [l.get ⟨n, h⟩] :=
  by
  rw [drop_eq_getElem_cons h, take, take]
  simp

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