Commit 2023-05-11 05:53 db6e42c2

View on Github →

feat: port Computability.Reduce (#3862)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/Reduce.lean

added theorem Computable.equiv₂

added theorem Computable.eqv

added theorem ComputablePred.computable_of_manyOneReducible

added theorem ComputablePred.computable_of_oneOneReducible

added theorem Equiv.Computable.symm

added theorem Equiv.Computable.trans

added theorem ManyOneDegree.add_of

added def ManyOneDegree.of

added theorem ManyOneDegree.of_eq_of

added theorem ManyOneDegree.of_le_of

added def ManyOneDegree

added theorem ManyOneEquiv.congr_left

added theorem ManyOneEquiv.congr_right

added theorem ManyOneEquiv.le_congr_left

added theorem ManyOneEquiv.le_congr_right

added theorem ManyOneEquiv.of_equiv

added theorem ManyOneEquiv.symm

added theorem ManyOneEquiv.trans

added def ManyOneEquiv

added theorem ManyOneReducible.mk

added theorem ManyOneReducible.trans

added def ManyOneReducible

added theorem OneOneEquiv.congr_left

added theorem OneOneEquiv.congr_right

added theorem OneOneEquiv.le_congr_left

added theorem OneOneEquiv.le_congr_right

added theorem OneOneEquiv.of_equiv

added theorem OneOneEquiv.symm

added theorem OneOneEquiv.to_many_one

added theorem OneOneEquiv.trans

added def OneOneEquiv

added theorem OneOneReducible.disjoin_left

added theorem OneOneReducible.disjoin_right

added theorem OneOneReducible.mk

added theorem OneOneReducible.of_equiv

added theorem OneOneReducible.of_equiv_symm

added theorem OneOneReducible.to_many_one

added theorem OneOneReducible.trans

added def OneOneReducible

added theorem Ulower.down_computable

added theorem disjoin_le

added theorem disjoin_manyOneReducible

added theorem equivalence_of_manyOneEquiv

added theorem equivalence_of_oneOneEquiv

added theorem manyOneEquiv_refl

added theorem manyOneEquiv_toNat

added theorem manyOneEquiv_up

added theorem manyOneReducible_refl

added theorem manyOneReducible_toNat

added theorem manyOneReducible_toNat_toNat

added theorem oneOneEquiv_refl

added theorem oneOneReducible_refl

added theorem reflexive_manyOneReducible

added theorem reflexive_oneOneReducible

added def toNat

added theorem toNat_manyOneEquiv

added theorem toNat_manyOneReducible

added theorem transitive_manyOneReducible

added theorem transitive_oneOneReducible