Commit 2022-02-16 19:16 5e3d465c

View on Github →

feat(category_theory/category/PartialFun): The category of types with partial functions (#11866) Define PartialFun, the category of types with partial functions, and show its equivalence with Pointed.

Estimated changes

Created src/category_theory/category/PartialFun.lean

added def PartialFun.iso.mk

added def PartialFun.of

added def PartialFun

added def Pointed_to_PartialFun

added def Type_to_PartialFun

Modified src/category_theory/category/Pointed.lean

added def Pointed.iso.mk

Modified src/data/subtype.lean

modified theorem exists_eq_subtype_mk_iff

modified theorem exists_subtype_mk_eq_iff

added theorem subtype.coe_inj

modified theorem subtype.coe_injective

added theorem subtype.val_inj

modified theorem subtype.val_injective