Mathlib Map

Theorems · Definition · logic and foundations

PFun.comp

{α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (β →. γ) → (α →. β) → α →. γ

Composition of partial functions as a partial function.

Defined in
Mathlib.Data.PFun
Cited by
10 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PFun.Part.bind_comp · cited by 1Part.bind_compPFun.coe_comp · cited by 0PFun.coe_compPFun.comp_apply · cited by 0PFun.comp_applyPFun.comp_assoc · cited by 0PFun.comp_assocPFun.comp_id · cited by 0PFun.comp_idPFun.preimage_comp · cited by 0PFun.preimage_compPFun.id_comp · cited by 0PFun.id_compPFun.dom_comp · cited by 0PFun.dom_compPFun.prodLift_fst_comp_snd_comp · cited by 0PFun.prodLift_fst_comp_sn…PFun.prodMap_comp_comp · cited by 0PFun.prodMap_comp_compPFun · cited by 207PFunPart.bind · cited by 70Part.bindPFun.compCITED BYCITES

Cites2

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

  • PFunstatement and proof · cited by 207
  • Part.bindproof · cited by 70

Cited by10

Results whose statement or proof uses this declaration.