Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-08 09:28 4444464c

View on Github →

feat(data/pfun): add restrict, preimage, core, etc.

Estimated changes

Modified src/data/pfun.lean

added theorem pfun.as_subtype_eq_of_mem

added theorem pfun.compl_dom_subset_core

added def pfun.core

added theorem pfun.core_def

added theorem pfun.core_eq

added theorem pfun.core_inter

added theorem pfun.core_mono

added theorem pfun.core_res

added theorem pfun.core_restrict

added theorem pfun.dom_eq

added def pfun.graph'

added def pfun.image

added theorem pfun.image_def

added theorem pfun.image_inter

added theorem pfun.image_mono

added theorem pfun.image_union

added theorem pfun.mem_core

added theorem pfun.mem_core_res

added theorem pfun.mem_dom

added theorem pfun.mem_image

added def pfun.mem_preimage

added theorem pfun.mem_res

added theorem pfun.mem_restrict

added def pfun.preimage

added theorem pfun.preimage_as_subtype

added theorem pfun.preimage_def

added theorem pfun.preimage_eq

added theorem pfun.preimage_inter

added theorem pfun.preimage_mono

added theorem pfun.preimage_subset_core

added theorem pfun.preimage_subset_dom

added theorem pfun.preimage_union

added theorem pfun.preimage_univ

added def pfun.res

added theorem pfun.res_univ

added theorem roption.mem_eq

added theorem roption.mem_restrict