drop_get? — Mathlib

English

Dropping the first n elements and then retrieving the m-th element equals retrieving the (n+m)-th element of the original sequence.

Русский

Пропуская первые n элементов и затем извлекая m-й элемент, получаем тот же результат, что и извлекая (n+m)-й элемент исходной последовательности.

LaTeX

$$$\forall {n m : \mathbb{N}} \; {s : Seq \alpha}, (s.drop n).get? m = s.get? (n + m)$$$

Lean4

@[simp]
theorem drop_get? {n m : ℕ} {s : Seq α} : (s.drop n).get? m = s.get? (n + m) := by
  induction n generalizing m with
  | zero => simp [drop]
  | succ k ih =>
    simp [Seq.get?_tail, drop]
    convert ih using 2
    cutsat

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