getElem?_toList — Mathlib

English

For a terminating sequence, the element at position n in toList equals the value s.get? n.

Русский

Для завершающейся последовательности элемент на позиции n в toList равен s.get? n.

LaTeX

$$$(\mathrm{toList}(s, h))[n]? = s.get? n$$$

Lean4

@[simp]
theorem getElem?_toList (s : Seq α) (h : s.Terminates) (n : ℕ) : (toList s h)[n]? = s.get? n :=
  by
  ext k
  simp only [toList, getElem?_take, Nat.lt_find_iff, length, Option.ite_none_right_eq_some, and_iff_right_iff_imp,
    TerminatedAt]
  intro h m hmn
  let ⟨a, ha⟩ := ge_stable s hmn h
  simp [ha]

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