mem_range_encode — Mathlib

English

The predicate n ∈ Set.range (encode : α → ℕ) is primitive recursive.

Русский

Предикат $n \in \mathrm{Set.range} (\mathrm{encode}): \alpha \to \mathbb{N}$ примитивно-рекурсивен.

LaTeX

$$$\operatorname{PrimrecPred}\big( n \mapsto n \in \mathrm{Set.range}(\mathrm{encode} : \alpha \to \mathbb{N}) \big)$$$

Lean4

theorem mem_range_encode : PrimrecPred (fun n => n ∈ Set.range (encode : α → ℕ)) :=
  have : PrimrecPred fun n => Encodable.decode₂ α n ≠ none :=
    .not
      (Primrec.eq.comp
        (.option_bind .decode
          (.ite (by simpa using Primrec.eq.comp (Primrec.encode.comp .snd) .fst) (Primrec.option_some.comp .snd)
            (.const _)))
        (.const _))
  this.of_eq fun _ => decode₂_ne_none_iff

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