Def Preorder.isInitialBot

Modification history

2025-11-01 00:46

Mathlib/CategoryTheory/Limits/Preorder.lean

feat(CategoryTheory): (Co)limits in preorders (#29253) …

Modified Preorder.isInitialBot View on Github →

2025-01-28 22:24

Mathlib/CategoryTheory/Limits/Preorder.lean

feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element (#21094) …

Modified Preorder.isInitialBot View on Github →

2025-01-24 08:30

Mathlib/CategoryTheory/Limits/Shapes/Preorder/Basic.lean

feat(CategoryTheory): (co)limits indexed by preorders (#20335) …

Added Preorder.isInitialBot View on Github →