Commit 2024-11-24 10:18 83ce5b01

View on Github →

feat(CategoryTheory/Over): more API for post (#19312)

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Over.lean

added def CategoryTheory.Over.mapCongr

added def CategoryTheory.Over.mapIso

added theorem CategoryTheory.Over.mapIso_functor

added theorem CategoryTheory.Over.mapIso_inverse

added def CategoryTheory.Over.opEquivOpUnder

added def CategoryTheory.Over.opToOpUnder

added def CategoryTheory.Over.opToUnderOp

added def CategoryTheory.Over.postComp

added def CategoryTheory.Over.postCongr

added def CategoryTheory.Over.postEquiv

added def CategoryTheory.Over.postMap

added theorem CategoryTheory.Over.post_comp

added def CategoryTheory.Under.mapCongr

added def CategoryTheory.Under.mapIso

added theorem CategoryTheory.Under.mapIso_functor

added theorem CategoryTheory.Under.mapIso_inverse

added def CategoryTheory.Under.opEquivOpOver

added def CategoryTheory.Under.opToOpOver

added def CategoryTheory.Under.opToOverOp

added def CategoryTheory.Under.postComp

added def CategoryTheory.Under.postCongr

added def CategoryTheory.Under.postEquiv

added def CategoryTheory.Under.postMap

added theorem CategoryTheory.Under.post_comp