to_re — Mathlib

English

If p is a computable predicate, then p is recursively enumerable (REPred p).

Русский

Если p — вычислимый предикат, то он рекурсивно перечислим.

LaTeX

$$$\forall \alpha\, [\text{Primcodable } \alpha],\; {p : \alpha \to \mathrm{Prop}}\; \mathrm{ComputablePred}(p) \Rightarrow \mathrm{REPred}(p).$$

Lean4

theorem to_re {p : α → Prop} (hp : ComputablePred p) : REPred p :=
  by
  obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp
  unfold REPred
  dsimp only []
  refine (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n => Part.ext fun a => ?_
  cases a; cases f n <;> simp

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