Theorem CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers

Modification history

2026-08-11 14:33
Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean
chore(CategoryTheory/Adjunction/AdjointFunctorTheorems): generalize universes (#41244) …
Modified CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizersView on Github →
2023-04-25 09:36
Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean
feat: port CategoryTheory.Limits.Constructions.WeaklyInitial (#3627)
Added CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizersView on Github →