Commit 2023-06-21 21:04 05a29ead

View on Github →

feat: port CategoryTheory.Category.PartialFun (#5301)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/PartialFun.lean

added def PartialFun.Iso.mk

added def PartialFun.of

added def PartialFun

added def pointedToPartialFun

added def typeToPartialFun

Modified Mathlib/Data/Option/Defs.lean

added theorem Option.elim'_eq_elim