Def CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty

Modification history

2025-05-18 17:44

Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

feat(AlgebraicGeometry): Inverse limit of nonempty schemes is nonempty (#24758)

Added CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty View on Github →