Theorems · Definition · logic and foundations

OneOneEquiv

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

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

Defined in

Mathlib.Computability.Reduce

Cited by

10 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

PrimcodablePrimcodable