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