Mathlib Map

Theorems · Theorem · logic and foundations

Nat.Partrec.of_eq

∀ {f g : ℕ →. ℕ}, Nat.Partrec f → (∀ (n : ℕ), f n = g n) → Nat.Partrec g
Defined in
Mathlib.Computability.Partrec
Cited by
14 results in Mathlib
Foundations
Depth 5 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Primrec.to_comp · cited by 40Primrec.to_compPartrec.comp · cited by 12Partrec.compPartrec.bind · cited by 10Partrec.bindComputable.ofOption · cited by 7Computable.ofOptionComputable.pair · cited by 5Computable.pairPartrec.rfind · cited by 4Partrec.rfindNat.Partrec.ppred · cited by 4Partrec.ppredPartrec.none · cited by 3Partrec.nonePartrec.nat_rec · cited by 3Partrec.nat_recPartrec.option_some_iff · cited by 2Partrec.option_some_iffNat.Partrec.none · cited by 2Partrec.noneNat.Partrec.prec' · cited by 1Partrec.prec'Computable.bind_decode_iff · cited by 1Computable.bind_decode_iffNat.Partrec.of_eq_tot · cited by 1Partrec.of_eq_totPart · cited by 325PartPFun · cited by 207PFunNat.Partrec · cited by 19Nat.PartrecPartrec.of_eqCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Partstatement · cited by 325
  • PFunstatement and proof · cited by 207
  • Nat.Partrecstatement and proof · cited by 19

Cited by14

Results whose statement or proof uses this declaration.