Theorems · Theorem · logic and foundations

ManyOneDegree.of_eq_of

∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {β : Type v} [inst_2 : Primcodable β]
  [inst_3 : Inhabited β] {p : α → Prop} {q : β → Prop}, ManyOneDegree.of p = ManyOneDegree.of q ↔ ManyOneEquiv p q

Defined in

Mathlib.Computability.Reduce

Cited by

1 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PrimcodableInhabitedPrimcodableInhabited