take_one_drop_eq_of_lt_length — Mathlib

English

If n is less than the length of l, then the first element after dropping n equals the nth element of l.

Русский

Если n меньше длины списка l, то первый элемент после пропуска n равен n-му элементу l.

LaTeX

$$$ (l.drop n).take 1 = [l.get \langle n, h \rangle] $, при условии h : n < l.length$$

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

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