Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-07 12:33 04b9d281

View on Github →

feat(data/pfun): Composition of partial functions (#11865) Define

  • pfun.id: The identity as a partial function
  • pfun.comp: Composition of partial functions
  • pfun.to_subtype: Restrict the codomain of a function to a subtype and make it partial

Estimated changes

added theorem part.bind_to_option
added theorem part.dom.of_bind
added theorem part.elim_to_option
added theorem part.mem_mk_iff
modified theorem part.some_inj
added theorem part.some_injective
added theorem part.bind_comp
added theorem pfun.bind_apply
added theorem pfun.coe_comp
added theorem pfun.coe_id
added theorem pfun.coe_injective
added def pfun.comp
added theorem pfun.comp_apply
added theorem pfun.comp_assoc
added theorem pfun.comp_id
added theorem pfun.dom_coe
added theorem pfun.dom_comp
added theorem pfun.dom_to_subtype
modified def pfun.fn
added theorem pfun.fn_apply
added theorem pfun.id_apply
added theorem pfun.id_comp
modified theorem pfun.mem_core
modified theorem pfun.mem_dom
modified theorem pfun.mem_preimage
added theorem pfun.preimage_comp
added def pfun.to_subtype
added theorem pfun.to_subtype_apply