list_getI — Mathlib

English

Under mild encoding assumptions (Primcodable α and Inhabited α), the function List.getI is Primrec₂.

Русский

При допустимых предположениях кодируемости и наличия элемента по умолчанию, функция List.getI является Primrec₂.

LaTeX

$$$\\operatorname{Primrec}_2(\\text{List.getI}_{\\alpha})$ (for all primcodable and inhabited $\\alpha$).$$

Lean4

theorem list_getI [Inhabited α] : Primrec₂ (@List.getI α _) :=
  list_getD _

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