cons_get_drop_succ — Mathlib

English

Let l be a list and n a finite index; for the pair (l, n) where n < length(l), the same relationship as above holds but with Fin indexing: l[n] :: l.drop (n+1) = l.drop n.

Русский

Пусть l — список и n— индекс, удовлетворяющий n < |l|. Тогда l[n] :: l.drop (n+1) = l.drop n (для индекса Fin).

LaTeX

$$$\\forall {\\{l : List\\,\\alpha\\}}, \\forall {n : Nat} {h : n < |l|}, \\, l[n] :: l.drop (n+1) = l.drop n$$$

Lean4

theorem cons_get_drop_succ {l : List α} {n} : l.get n :: l.drop (n.1 + 1) = l.drop n.1 :=
  (drop_eq_getElem_cons n.2).symm

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