Def CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty

Modification history

2026-08-17 12:02
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
chore(CategoryTheory/Limits/Shapes/Terminal): use `to_dual` (#42842) …
Deleted CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmptyView on Github →
2025-12-13 14:21
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmptyView on Github →
2025-05-18 17:44
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
feat(AlgebraicGeometry): Inverse limit of nonempty schemes is nonempty (#24758)
Added CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmptyView on Github →