re_pred_and
theoremverified
If p and q are recursively enumerable predicates, then their conjunction fun a => p a ∧ q a is recursively enumerable.
Statement
theorem re_pred_and {α : Type*} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred (fun a => p a ∧ q a)
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext
Lean source view module on GitHub
/-- Conjunction of two recursively enumerable predicates is recursively enumerable. -/ theorem re_pred_and {α : Type*} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred (fun a => p a ∧ q a) := by have hg : Partrec₂ (fun (a : α) (_ : Unit) => Part.assert (q a) fun _ => Part.some ()) := hq.comp Computable.fst have h := hp.bind hg refine h.of_eq fun a => ?_ apply Part.ext intro u simp [Part.mem_assert_iff, Part.mem_bind_iff]