not_re_of_manyOneReducible_and_not_re
theoremverified
If p is many-one reducible to q and p is not recursively enumerable, then q is not recursively enumerable.
Statement
theorem not_re_of_manyOneReducible_and_not_re {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h : p ≤₀ q) (hp : ¬REPred p) : ¬REPred q
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- re_of_manyOneReducibleIf `p` is many-one reducible to `q` and `q` is recursively enumerable, then `p` is recursively enumerable.
Lean source view module on GitHub
/-- If p reduces to q and p is not RE, then q is not RE. -/ theorem not_re_of_manyOneReducible_and_not_re {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h : p ≤₀ q) (hp : ¬REPred p) : ¬REPred q := by intro hq exact hp (re_of_manyOneReducible h hq)