Commit 2023-02-21 19:52 f327ca89

View on Github →

feat: port/CategoryTheory.PEmpty (#2363)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/PEmpty.lean

added def CategoryTheory.Functor.empty

added def CategoryTheory.Functor.emptyEquivalence

added def CategoryTheory.Functor.emptyExt

added theorem CategoryTheory.Functor.empty_ext'

added def CategoryTheory.Functor.uniqueFromEmpty