get?_enum — Mathlib

English

For any sequence s and index n, the nth element of the enumeration enum(s) equals the nth element of s paired with n, when defined.

Русский

Для любой последовательности s и индекса n, n-й элемент перечисления enum(s) равен пары (n, s_n), если она определена.

LaTeX

$$$$ \\mathrm{get?}(\\mathrm{enum}(s))\\ n = \\mathrm{map}(\\mathrm{Prod.mk}\\, n)\\bigl(\\mathrm{get?}s\\,n\\bigr). $$$$

Lean4

@[simp]
theorem get?_enum (s : Seq α) (n : ℕ) : get? (enum s) n = Option.map (Prod.mk n) (get? s n) :=
  get?_zip _ _ _

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