Mathlib Map

Theorems · Theorem · logic and foundations

Partrec.of_eq

∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α →. σ},
  Partrec f → (∀ (n : α), f n = g n) → Partrec g
Defined in
Mathlib.Computability.Partrec
Cited by
19 results in Mathlib
Foundations
Depth 11 from the axioms · uses Quot.sound
Assumes
PrimcodablePrimcodable
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Partrec.to₂ · cited by 9Partrec.to₂Nat.Partrec.Code.eval_part · cited by 5Code.eval_partPartrec.cond · cited by 3Partrec.condPartrec.sumCasesOn_right · cited by 3Partrec.sumCasesOn_rightPartrec.nat_casesOn_right · cited by 2Partrec.nat_casesOn_rightDecidable.Partrec.const' · cited by 2Partrec.const'Computable.nat_rec · cited by 2Computable.nat_recPartrec.of_eq_tot · cited by 2Partrec.of_eq_totComputable.bind_decode_iff · cited by 1Computable.bind_decode_iffComputablePred.computable_iff_re_compl_re · cited by 1ComputablePred.computable…Partrec.dom_re · cited by 1Partrec.dom_reComputablePred.to_re · cited by 1ComputablePred.to_rePartrec.optionCasesOn_right · cited by 1Partrec.optionCasesOn_rig…Partrec.sumCasesOn_left · cited by 1Partrec.sumCasesOn_leftComputable.vector_ofFn · cited by 1Computable.vector_ofFnPrimcodable · cited by 325PrimcodablePart · cited by 325PartPFun · cited by 207PFunPartrec · cited by 48PartrecPartrec.of_eqCITED BYCITES

Cites4

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

  • Primcodablestatement and proof · cited by 325
  • Partstatement · cited by 325
  • PFunstatement and proof · cited by 207
  • Partrecstatement and proof · cited by 48

Cited by19

Results whose statement or proof uses this declaration.