get? — Mathlib

English

For any sequence s and any natural number n, the nth element is obtained as an element of the underlying sequence representation, i.e., get? s n yields the nth element if it exists.

Русский

Для любой последовательности s и любого натурального числа n n-й элемент определяется как элемент базового представления последовательности: get? s n даёт n-й элемент, если он существует.

LaTeX

$$$\\operatorname{get?}(s,n) = s\\;\\mathrm{val}(n). $$$

Lean4

/-- Get the nth element of a sequence (if it exists) -/
def get? : Seq α → ℕ → Option α :=
  Subtype.val

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