list_getD — Mathlib

English

For any d, the two-argument function (l, n) ↦ List.getD l n d is primitive recursive.

Русский

Для любого элемента d отображение (l,n) ↦ List.getD l n d примитивно вычислимо.

LaTeX

$$$\\mathrm{Primrec}_2\\big( (l,n) \\mapsto \\mathrm{List}.\\mathrm{getD}(l,n,d) \\big) \\quad(d\\text{ фиксировано})$$$

Lean4

theorem list_getD (d : α) : Primrec₂ fun l n => List.getD l n d :=
  by
  simp only [List.getD_eq_getElem?_getD]
  exact option_getD.comp₂ list_getElem? (const _)

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