not_computable_of_manyOneReducible
theoremverified
If `p` is many-one reducible to `q` and `p` is undecidable (not computable), then `q` is undecidable.
Statement
theorem not_computable_of_manyOneReducible {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : ¬ComputablePred p) : ¬ComputablePred q
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext
Lean source view module on GitHub
/-- Undecidability transfers forward under many-one reductions. -/ theorem not_computable_of_manyOneReducible {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : ¬ComputablePred p) : ¬ComputablePred q := mt (ComputablePred.computable_of_manyOneReducible h₁) h₂