dom_finite — Mathlib

English

If the domain α is finite, every function f: α → σ is primitive recursive.

Русский

Если область определения α конечна, любая функция f: α→σ примитивно вычисима.

LaTeX

$$$[Finite\\alpha]\\; (f:\\alpha\\to\\sigma) \\Rightarrow Primrec f$$$

Lean4

theorem dom_finite [Finite α] (f : α → σ) : Primrec f :=
  let ⟨l, _, m⟩ := Finite.exists_univ_list α
  option_some_iff.1 <| by
    haveI := decidableEqOfEncodable α
    refine ((list_getElem?₁ (l.map f)).comp (list_idxOf₁ l)).of_eq fun a => ?_
    rw [List.getElem?_map, List.getElem?_idxOf (m a), Option.map_some]

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