dropn_cons — Mathlib

English

For any a, s, n, dropping n+1 from cons(a,s) equals dropping n from s.

Русский

Пусть a : α, s — WSeq α. Опускание n+1 элементов из cons(a,s) равно опусканию n элементов из s.

LaTeX

$$$$\operatorname{drop}(\operatorname{cons}(a,s), n+1) = \operatorname{drop}(s,n).$$$$

Lean4

@[simp]
theorem dropn_cons (a : α) (s) (n) : drop (cons a s) (n + 1) = drop s n := by
  induction n with
  | zero => simp [drop]
  | succ n n_ih => simp [drop, ← n_ih]

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