Theorems · Definition · logic and foundations

OneOneReducible

{α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → Prop) → (β → Prop) → Prop

p is one-one reducible to q if there is an injective computable function translating questions about p to questions about q.

Defined in

Mathlib.Computability.Reduce

Cited by

15 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

PrimcodablePrimcodable