Def CategoryTheory.createsLimitOfReflectsIso'

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.createsLimitOfReflectsIso'View on Github →

2024-03-18 21:07

Mathlib/CategoryTheory/Limits/Creates.lean

feat: functor creates limit if it lifts a single limit cone (#11482)

Added CategoryTheory.createsLimitOfReflectsIso'View on Github →