Theorems · Definition · logic and foundations
ComputablePred
{α : Type u_1} → [Primcodable α] → (α → Prop) → PropA computable predicate is one whose indicator function is computable.
- Defined in
- Mathlib.Computability.RE
- Cited by
- 17 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.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Primcodablestatement and proof · cited by 325
- Computableproof · cited by 80
Cited by17
Results whose statement or proof uses this declaration.
- Computable.computablePredstatement · cited by 3
- ComputablePred.decidestatement and proof · cited by 3
- ComputablePred.computable_iffstatement and proof · cited by 2
- ComputablePred.ricestatement and proof · cited by 2
- ComputablePred.computable_iff_re_compl_restatement and proof · cited by 1
- ComputablePred.computable_iff_re_compl_re'statement · cited by 1
- ComputablePred.computable_of_manyOneReduciblestatement and proof · cited by 1
- ComputablePred.halting_problemstatement and proof · cited by 1
- ComputablePred.notstatement and proof · cited by 1
- ComputablePred.of_eqstatement and proof · cited by 1
- ComputablePred.to_restatement and proof · cited by 1
- ComputablePred.computable_of_oneOneReduciblestatement · cited by 0