Commit 2023-02-02 11:02 b5c7d54d

View on Github →

feat: port data.pfun (#1179) Port of data.pfun

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/PFun.lean

added def PFun.Dom

added theorem PFun.Part.bind_comp

added theorem PFun.Preimage_def

added def PFun.asSubtype

added theorem PFun.asSubtype_eq_of_mem

added def PFun.bind

added theorem PFun.bind_apply

added theorem PFun.bind_defined

added theorem PFun.coe_comp

added theorem PFun.coe_id

added theorem PFun.coe_preimage

added theorem PFun.coe_val

added def PFun.comp

added theorem PFun.comp_apply

added theorem PFun.comp_assoc

added theorem PFun.comp_id

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_coe

added theorem PFun.dom_comp

added theorem PFun.dom_eq

added theorem PFun.dom_iff_graph

added theorem PFun.dom_mk

added theorem PFun.dom_of_mem_fix

added theorem PFun.dom_prodLift

added theorem PFun.dom_prodMap

added theorem PFun.dom_to_subtype

added theorem PFun.dom_to_subtype_apply_iff

added def PFun.equivSubtype

added def PFun.evalOpt

added theorem PFun.ext'

added theorem PFun.ext

added theorem PFun.fixInduction'_fwd

added theorem PFun.fixInduction'_stop

added theorem PFun.fixInduction_spec

added theorem PFun.fix_fwd

added theorem PFun.fix_fwd_eq

added theorem PFun.fix_stop

added def PFun.fn

added theorem PFun.fn_apply

added theorem PFun.get_prodLift

added theorem PFun.get_prodMap

added def PFun.graph'

added def PFun.graph

added theorem PFun.id_apply

added theorem PFun.id_comp

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.lift_graph

added theorem PFun.lift_injective

added def PFun.map

added theorem PFun.mem_core

added theorem PFun.mem_core_res

added theorem PFun.mem_dom

added theorem PFun.mem_fix_iff

added theorem PFun.mem_image

added theorem PFun.mem_preimage

added theorem PFun.mem_prodLift

added theorem PFun.mem_prodMap

added theorem PFun.mem_res

added theorem PFun.mem_restrict

added theorem PFun.mem_to_subtype_iff

added def PFun.preimage

added theorem PFun.preimage_as_subtype

added theorem PFun.preimage_comp

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.prodLift

added theorem PFun.prodLift_apply

added theorem PFun.prodLift_fst_comp_snd_comp

added def PFun.prodMap

added theorem PFun.prodMap_apply

added theorem PFun.prodMap_comp_comp

added theorem PFun.prodMap_id_id

added theorem PFun.pure_defined

added def PFun.ran

added def PFun.res

added theorem PFun.res_univ

added def PFun.restrict

added def PFun.toSubtype

added theorem PFun.to_subtype_apply

added def PFun