Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-02-21 07:31
23092673
View on Github →
feat: port CategoryTheory.Category.Ulift (
#2312
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Category/ULift.lean
added
def
CategoryTheory.AsSmall.down
added
def
CategoryTheory.AsSmall.equiv
added
def
CategoryTheory.AsSmall.up
added
def
CategoryTheory.AsSmall.{w,
added
def
CategoryTheory.ULift.downFunctor
added
def
CategoryTheory.ULift.equivalence
added
def
CategoryTheory.ULift.upFunctor
added
def
CategoryTheory.ULiftHom.down
added
def
CategoryTheory.ULiftHom.equiv
added
def
CategoryTheory.ULiftHom.objDown
added
def
CategoryTheory.ULiftHom.objUp
added
def
CategoryTheory.ULiftHom.up
added
def
CategoryTheory.ULiftHom.{w,u}
added
def
CategoryTheory.ULiftHomULiftCategory.equiv.{v',
added
theorem
CategoryTheory.objDown_objUp
added
theorem
CategoryTheory.objUp_objDown