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

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