Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-16 14:03 c3d943e2

View on Github →

feat(computability): strong reducibility and degrees (#1203)

Estimated changes

Modified docs/references.bib

Modified src/computability/halting.lean

Modified src/computability/partrec.lean

Modified src/computability/partrec_code.lean

added theorem nat.partrec.code.injective_const

added theorem nat.partrec.code.injective_curry

added theorem nat.partrec.code.smn

Modified src/computability/primrec.lean

Created src/computability/reduce.lean

added theorem computable.equiv₂

added theorem computable.eqv

added theorem computable_pred.computable_of_many_one_reducible

added theorem computable_pred.computable_of_one_one_reducible

added theorem disjoin_le

added theorem disjoin_many_one_reducible

added theorem equiv.computable.symm

added theorem equiv.computable.trans

added def equiv.computable

added theorem equivalence_of_many_one_equiv

added theorem equivalence_of_one_one_equiv

added def many_one_degree.add

added theorem many_one_degree.add_le'

added theorem many_one_degree.add_le

added def many_one_degree.comap

added def many_one_degree.le

added theorem many_one_degree.le_add_left'

added theorem many_one_degree.le_add_left

added theorem many_one_degree.le_add_right'

added theorem many_one_degree.le_add_right

added theorem many_one_degree.le_antisymm

added theorem many_one_degree.le_comap_left

added theorem many_one_degree.le_comap_right

added theorem many_one_degree.le_refl

added theorem many_one_degree.le_trans

added def many_one_degree.of

added theorem many_one_degree.of_le_of'

added theorem many_one_degree.of_le_of

added def many_one_degree

added theorem many_one_equiv.congr_left

added theorem many_one_equiv.congr_right

added theorem many_one_equiv.le_congr_left

added theorem many_one_equiv.le_congr_right

added theorem many_one_equiv.of_equiv

added theorem many_one_equiv.symm

added theorem many_one_equiv.trans

added def many_one_equiv

added theorem many_one_equiv_refl

added def many_one_equiv_setoid

added theorem many_one_reducible.mk

added theorem many_one_reducible.trans

added def many_one_reducible

added theorem many_one_reducible_refl

added theorem one_one_equiv.congr_left

added theorem one_one_equiv.congr_right

added theorem one_one_equiv.le_congr_left

added theorem one_one_equiv.le_congr_right

added theorem one_one_equiv.of_equiv

added theorem one_one_equiv.symm

added theorem one_one_equiv.to_many_one

added theorem one_one_equiv.trans

added def one_one_equiv

added theorem one_one_equiv_refl

added theorem one_one_reducible.disjoin_left

added theorem one_one_reducible.disjoin_right

added theorem one_one_reducible.mk

added theorem one_one_reducible.of_equiv

added theorem one_one_reducible.of_equiv_symm

added theorem one_one_reducible.to_many_one

added theorem one_one_reducible.trans

added def one_one_reducible

added theorem one_one_reducible_refl

added theorem reflexive_many_one_reducible

added theorem reflexive_one_one_reducible

added theorem transitive_many_one_reducible

added theorem transitive_one_one_reducible