Def CategoryTheory.createsLimitOfFullyFaithfulOfIso'

Modification history

2024-04-12 14:33

Mathlib/CategoryTheory/Limits/Creates.lean

chore(CategoryTheory): move Full, Faithful, EssSurj, IsEquivalence and ReflectsIsomorphisms to the Functor namespace (#11985) …

Modified CategoryTheory.createsLimitOfFullyFaithfulOfIso'View on Github →

2023-03-06 07:28

Mathlib/CategoryTheory/Limits/Creates.lean

feat: port CategoryTheory.Limits.Creates (#2646)

Added CategoryTheory.createsLimitOfFullyFaithfulOfIso'View on Github →