Documentation Verification Report

Reduce

📁 Source: Mathlib/Computability/Reduce.lean

Statistics

Metric	Count
Definitions `Computable`, `ManyOneDegree`, `instAdd`, `instInhabited`, `instLE`, `instPartialOrder`, `instSemilatticeSup`, `liftOn`, `liftOn₂`, `of`, `ManyOneEquiv`, `ManyOneReducible`, `OneOneEquiv`, `OneOneReducible`, `toNat`, `«term_≤₀_»`, `«term_≤₁_»`	17
Theorems `equiv₂`, `eqv`, `computable_of_manyOneReducible`, `computable_of_oneOneReducible`, `trans`, `add_le`, `add_of`, `ind_on`, `le_add_left`, `le_add_right`, `liftOn_eq`, `liftOn₂_eq`, `of_eq_of`, `of_le_of`, `congr_left`, `congr_right`, `le_congr_left`, `le_congr_right`, `of_equiv`, `trans`, `mk`, `trans`, `congr_left`, `congr_right`, `le_congr_left`, `le_congr_right`, `of_equiv`, `to_many_one`, `trans`, `disjoin_left`, `disjoin_right`, `mk`, `of_equiv`, `of_equiv_symm`, `to_many_one`, `trans`, `down_computable`, `disjoin_le`, `disjoin_manyOneReducible`, `equivalence_of_manyOneEquiv`, `equivalence_of_oneOneEquiv`, `manyOneEquiv_refl`, `manyOneEquiv_toNat`, `manyOneEquiv_up`, `manyOneReducible_refl`, `manyOneReducible_toNat`, `manyOneReducible_toNat_toNat`, `oneOneEquiv_refl`, `oneOneReducible_refl`, `reflexive_manyOneReducible`, `reflexive_oneOneReducible`, `toNat_manyOneEquiv`, `toNat_manyOneReducible`, `transitive_manyOneReducible`, `transitive_oneOneReducible`	55
Total	72

Computable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv₂` 📖	mathematical	—	`Equiv.Computable` `Primcodable.ofDenumerable` `Denumerable.equiv₂`	—	`Equiv.Computable.trans` `eqv` `Equiv.Computable.symm`
`eqv` 📖	mathematical	—	`Equiv.Computable` `Primcodable.ofDenumerable` `Denumerable.nat` `Denumerable.eqv`	—	`encode` `ofNat`

ComputablePred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`computable_of_manyOneReducible` 📖	—	`ManyOneReducible` `ComputablePred`	—	—	`Set.ext` `computable_iff` `Computable.comp`
`computable_of_oneOneReducible` 📖	—	`OneOneReducible` `ComputablePred`	—	—	`computable_of_manyOneReducible` `OneOneReducible.to_many_one`

Equiv

Definitions

Name	Category	Theorems
`Computable` 📖	MathDef	3 math math: `ULower.down_computable`, `Computable.eqv`, `Computable.equiv₂`

Equiv.Computable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans` 📖	mathematical	`Equiv.Computable`	`Equiv.trans`	—	`Computable.comp`

ManyOneDegree

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	4 math math: `add_le`, `add_of`, `le_add_left`, `le_add_right`
`instInhabited` 📖	CompOp	—
`instLE` 📖	CompOp	4 math math: `add_le`, `le_add_left`, `of_le_of`, `le_add_right`
`instPartialOrder` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`liftOn` 📖	CompOp	1 math math: `liftOn_eq`
`liftOn₂` 📖	CompOp	1 math math: `liftOn₂_eq`
`of` 📖	CompOp	5 math math: `liftOn₂_eq`, `liftOn_eq`, `of_eq_of`, `add_of`, `of_le_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_le` 📖	mathematical	—	`ManyOneDegree` `instLE` `instAdd`	—	`ind_on` `disjoin_le`
`add_of` 📖	mathematical	—	`of` `Primcodable.sum` `Sum.instMonad_mathlib` `ManyOneDegree` `instAdd`	—	`of_eq_of` `disjoin_manyOneReducible` `ManyOneReducible.trans` `manyOneReducible_toNat` `OneOneReducible.to_many_one` `OneOneReducible.disjoin_left` `OneOneReducible.disjoin_right` `toNat_manyOneReducible`
`ind_on` 📖	—	`of` `Primcodable.ofDenumerable` `Denumerable.nat`	—	—	`Quotient.inductionOn'`
`le_add_left` 📖	mathematical	—	`ManyOneDegree` `instLE` `instAdd`	—	`add_le`
`le_add_right` 📖	mathematical	—	`ManyOneDegree` `instLE` `instAdd`	—	`add_le`
`liftOn_eq` 📖	mathematical	—	`liftOn` `of` `Primcodable.ofDenumerable` `Denumerable.nat`	—	—
`liftOn₂_eq` 📖	mathematical	—	`liftOn₂` `of` `Primcodable.ofDenumerable` `Denumerable.nat`	—	—
`of_eq_of` 📖	mathematical	—	`of` `ManyOneEquiv`	—	`of.eq_1` `Quotient.eq''`
`of_le_of` 📖	mathematical	—	`ManyOneDegree` `instLE` `of` `ManyOneReducible`	—	`manyOneReducible_toNat_toNat`

ManyOneEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_left` 📖	—	`ManyOneEquiv`	—	—	`le_congr_left` `le_congr_right`
`congr_right` 📖	—	`ManyOneEquiv`	—	—	`le_congr_right` `le_congr_left`
`le_congr_left` 📖	mathematical	`ManyOneEquiv`	`ManyOneReducible`	—	`ManyOneReducible.trans`
`le_congr_right` 📖	mathematical	`ManyOneEquiv`	`ManyOneReducible`	—	`ManyOneReducible.trans`
`of_equiv` 📖	mathematical	`Equiv.Computable`	`ManyOneEquiv` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`OneOneEquiv.to_many_one` `OneOneEquiv.of_equiv`
`trans` 📖	—	`ManyOneEquiv`	—	—	`ManyOneReducible.trans`

ManyOneReducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk` 📖	mathematical	`Computable`	`ManyOneReducible`	—	—
`trans` 📖	—	`ManyOneReducible`	—	—	`Computable.comp`

OneOneEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_left` 📖	—	`OneOneEquiv`	—	—	`le_congr_left` `le_congr_right`
`congr_right` 📖	—	`OneOneEquiv`	—	—	`le_congr_right` `le_congr_left`
`le_congr_left` 📖	mathematical	`OneOneEquiv`	`OneOneReducible`	—	`OneOneReducible.trans`
`le_congr_right` 📖	mathematical	`OneOneEquiv`	`OneOneReducible`	—	`OneOneReducible.trans`
`of_equiv` 📖	mathematical	`Equiv.Computable`	`OneOneEquiv` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`OneOneReducible.of_equiv` `OneOneReducible.of_equiv_symm`
`to_many_one` 📖	mathematical	`OneOneEquiv`	`ManyOneEquiv`	—	`OneOneReducible.to_many_one`
`trans` 📖	—	`OneOneEquiv`	—	—	`OneOneReducible.trans`

OneOneReducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoin_left` 📖	mathematical	—	`OneOneReducible` `Primcodable.sum`	—	`Computable.sumInl`
`disjoin_right` 📖	mathematical	—	`OneOneReducible` `Primcodable.sum`	—	`Computable.sumInr`
`mk` 📖	mathematical	`Computable`	`OneOneReducible`	—	—
`of_equiv` 📖	mathematical	`Computable` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`OneOneReducible`	—	`Equiv.injective`
`of_equiv_symm` 📖	mathematical	`Computable` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	`OneOneReducible`	—	`Equiv.apply_symm_apply` `of_equiv`
`to_many_one` 📖	mathematical	`OneOneReducible`	`ManyOneReducible`	—	—
`trans` 📖	—	`OneOneReducible`	—	—	`Computable.comp`

ULower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_computable` 📖	mathematical	—	`Equiv.Computable` `ULower` `Primcodable.toEncodable` `Primcodable.ulower` `equiv`	—	`Primrec.to_comp` `Primrec.ulower_down` `Primrec.ulower_up`

(root)

Definitions

Name	Category	Theorems
`ManyOneDegree` 📖	CompOp	5 math math: `ManyOneDegree.add_le`, `ManyOneDegree.add_of`, `ManyOneDegree.le_add_left`, `ManyOneDegree.of_le_of`, `ManyOneDegree.le_add_right`
`ManyOneEquiv` 📖	MathDef	8 math math: `equivalence_of_manyOneEquiv`, `ManyOneEquiv.of_equiv`, `OneOneEquiv.to_many_one`, `ManyOneDegree.of_eq_of`, `manyOneEquiv_refl`, `manyOneEquiv_toNat`, `manyOneEquiv_up`, `toNat_manyOneEquiv`
`ManyOneReducible` 📖	MathDef	12 math math: `disjoin_le`, `OneOneReducible.to_many_one`, `transitive_manyOneReducible`, `ManyOneEquiv.le_congr_right`, `manyOneReducible_refl`, `ManyOneEquiv.le_congr_left`, `manyOneReducible_toNat_toNat`, `reflexive_manyOneReducible`, `manyOneReducible_toNat`, `toNat_manyOneReducible`, `ManyOneDegree.of_le_of`, `ManyOneReducible.mk`
`OneOneEquiv` 📖	MathDef	3 math math: `oneOneEquiv_refl`, `equivalence_of_oneOneEquiv`, `OneOneEquiv.of_equiv`
`OneOneReducible` 📖	MathDef	10 math math: `OneOneReducible.of_equiv`, `OneOneEquiv.le_congr_left`, `OneOneReducible.mk`, `transitive_oneOneReducible`, `OneOneReducible.of_equiv_symm`, `OneOneReducible.disjoin_left`, `oneOneReducible_refl`, `reflexive_oneOneReducible`, `OneOneReducible.disjoin_right`, `OneOneEquiv.le_congr_right`
`toNat` 📖	CompOp	5 math math: `manyOneReducible_toNat_toNat`, `manyOneReducible_toNat`, `manyOneEquiv_toNat`, `toNat_manyOneReducible`, `toNat_manyOneEquiv`
`«term_≤₀_»` 📖	CompOp	—
`«term_≤₁_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoin_le` 📖	mathematical	—	`ManyOneReducible` `Primcodable.sum`	—	`ManyOneReducible.trans` `OneOneReducible.to_many_one` `OneOneReducible.disjoin_left` `OneOneReducible.disjoin_right` `disjoin_manyOneReducible`
`disjoin_manyOneReducible` 📖	mathematical	`ManyOneReducible`	`Primcodable.sum`	—	`Computable.sumCasesOn` `Computable.id` `Computable.to₂` `Computable.comp` `Computable.snd`
`equivalence_of_manyOneEquiv` 📖	mathematical	—	`ManyOneEquiv`	—	`manyOneEquiv_refl` `ManyOneEquiv.symm` `ManyOneEquiv.trans`
`equivalence_of_oneOneEquiv` 📖	mathematical	—	`OneOneEquiv`	—	`oneOneEquiv_refl` `OneOneEquiv.symm` `OneOneEquiv.trans`
`manyOneEquiv_refl` 📖	mathematical	—	`ManyOneEquiv`	—	`manyOneReducible_refl`
`manyOneEquiv_toNat` 📖	mathematical	—	`ManyOneEquiv` `Primcodable.ofDenumerable` `Denumerable.nat` `toNat`	—	—
`manyOneEquiv_up` 📖	mathematical	—	`ManyOneEquiv` `ULower` `Primcodable.toEncodable` `Primcodable.ulower` `ULower.up`	—	`ManyOneEquiv.of_equiv` `Equiv.Computable.symm` `ULower.down_computable`
`manyOneReducible_refl` 📖	mathematical	—	`ManyOneReducible`	—	`Computable.id`
`manyOneReducible_toNat` 📖	mathematical	—	`ManyOneReducible` `Primcodable.ofDenumerable` `Denumerable.nat` `toNat`	—	`Computable.encode` `Encodable.encodek`
`manyOneReducible_toNat_toNat` 📖	mathematical	—	`ManyOneReducible` `Primcodable.ofDenumerable` `Denumerable.nat` `toNat`	—	`ManyOneReducible.trans` `manyOneReducible_toNat` `toNat_manyOneReducible`
`oneOneEquiv_refl` 📖	mathematical	—	`OneOneEquiv`	—	`oneOneReducible_refl`
`oneOneReducible_refl` 📖	mathematical	—	`OneOneReducible`	—	`Computable.id`
`reflexive_manyOneReducible` 📖	mathematical	—	`Reflexive` `ManyOneReducible`	—	`manyOneReducible_refl`
`reflexive_oneOneReducible` 📖	mathematical	—	`Reflexive` `OneOneReducible`	—	`oneOneReducible_refl`
`toNat_manyOneEquiv` 📖	mathematical	—	`ManyOneEquiv` `Primcodable.ofDenumerable` `Denumerable.nat` `toNat`	—	—
`toNat_manyOneReducible` 📖	mathematical	—	`ManyOneReducible` `Primcodable.ofDenumerable` `Denumerable.nat` `toNat`	—	`Computable.option_getD` `Computable.decode` `Computable.const`
`transitive_manyOneReducible` 📖	mathematical	—	`Transitive` `ManyOneReducible`	—	`ManyOneReducible.trans`
`transitive_oneOneReducible` 📖	mathematical	—	`Transitive` `OneOneReducible`	—	`OneOneReducible.trans`

---

← Back to Index