val_eq_get — Mathlib

English

For every sequence s and every index n, the nth value of the underlying representation, s.val(n), agrees with get? s n.

Русский

Для каждой последовательности s и каждого индекса n выполняется равенство s.val(n) = get? s n.

LaTeX

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

Lean4

@[simp]
theorem val_eq_get (s : Seq α) (n : ℕ) : s.val n = s.get? n :=
  rfl

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