Theorems · Definition · logic and foundations

ManyOneEquiv

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

p and q are many-one equivalent if each one is many-one reducible to the other.

Defined in

Mathlib.Computability.Reduce

Cited by

16 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

PrimcodablePrimcodable