Commit 2023-04-25 11:42 234b9c19

View on Github →

feat: port CategoryTheory.Adjunction.AdjointFunctorTheorems (#3628)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

added theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating

added theorem CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating

added def CategoryTheory.SolutionSetCondition

added theorem CategoryTheory.solutionSetCondition_of_isRightAdjoint