Theorems · Definition · logic and foundations
REPred
{α : Type u_1} → [Primcodable α] → (α → Prop) → PropA recursively enumerable predicate is one which is the domain of a computable partial function.
- Defined in
- Mathlib.Computability.RE
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Primcodable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Primcodablestatement and proof · cited by 325
- Part.someproof · cited by 111
- Partrecproof · cited by 48
- Part.assertproof · cited by 10
Cited by7
Results whose statement or proof uses this declaration.
- ComputablePred.computable_iff_re_compl_restatement and proof · cited by 1
- ComputablePred.computable_iff_re_compl_re'statement · cited by 1
- ComputablePred.halting_problem_restatement · cited by 1
- Partrec.dom_restatement · cited by 1
- ComputablePred.to_restatement · cited by 1
- ComputablePred.halting_problem_not_restatement and proof · cited by 0
- REPred.of_eqstatement and proof · cited by 0