Theorem CategoryTheory.Functor.RepresentableBy.isRepresentable

Modification history

2024-10-04 10:12

Mathlib/CategoryTheory/Yoneda.lean

refactor(CategoryTheory): generalize universes for representable functors (#17389) …

Added CategoryTheory.Functor.RepresentableBy.isRepresentable View on Github →