Retracts

📁 Source: Mathlib/CategoryTheory/Presentable/Retracts.lean

Statistics

Metric	Count
Definitions	0
Theorems isCardinalPresentable, instIsStableUnderRetractsIsCardinalPresentable	2
Total	2

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStableUnderRetractsIsCardinalPresentable 📖	mathematical	—	ObjectProperty.IsStableUnderRetracts isCardinalPresentable	—	isCardinalPresentable_iff Retract.isCardinalPresentable

CategoryTheory.Retract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCardinalPresentable 📖	mathematical	—	CategoryTheory.IsCardinalPresentable	—	CategoryTheory.essentiallySmallSelf CategoryTheory.isFiltered_of_isCardinalFiltered CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit CategoryTheory.Category.assoc retract_assoc CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit' CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi instIsSplitEpiR

---

← Back to Index