re_of_manyOneReducible
theoremverified
If `p` is many-one reducible to `q` and `q` is recursively enumerable, then `p` is recursively enumerable.
Statement
theorem re_of_manyOneReducible {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : REPred q) : REPred p
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Used by 1
- not_re_of_manyOneReducible_and_not_reIf p is many-one reducible to q and p is not recursively enumerable, then q is not recursively enumerable.
Lean source view module on GitHub
/-- Recursive enumerability is preserved backwards under many-one reductions. -/ theorem re_of_manyOneReducible {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : REPred q) : REPred p := by obtain ⟨f, hf, hpq⟩ := h₁ have hqf : REPred (q ∘ f) := Partrec.comp h₂ hf exact REPred.of_eq hqf fun a => (hpq a).symm