Theorem CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating

Modification history

2026-08-11 14:33
Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
chore(CategoryTheory/Adjunction/AdjointFunctorTheorems): generalize universes (#41244) …
Modified CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparatingView on Github →
2025-10-27 15:31
Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
refactor(CategoryTheory/Generator): use ObjectProperty instead of Set (#30269) …
Modified CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparatingView on Github →
2024-12-23 08:45
Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
chore(CategoryTheory): generalize universes for WellPowered (#19992) …
Modified CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparatingView on Github →
2023-04-25 11:42
Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
feat: port CategoryTheory.Adjunction.AdjointFunctorTheorems (#3628)
Added CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparatingView on Github →