Def CategoryTheory.Functor.leftAdjointObjIsDefined

Modification history

2025-04-23 10:36

Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean

refactor(CategoryTheory): redefine full subcategories using `ObjectProperty` (#22574) …

Added CategoryTheory.Functor.leftAdjointObjIsDefined View on Github →