Def Preorder.isTerminalBot

Modification history

2025-01-28 22:24
Mathlib/CategoryTheory/Limits/Shapes/Preorder/Basic.lean
feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element (#21094) …
Deleted Preorder.isTerminalBotView on Github →
2025-01-24 08:30
Mathlib/CategoryTheory/Limits/Shapes/Preorder/Basic.lean
feat(CategoryTheory): (co)limits indexed by preorders (#20335) …
Added Preorder.isTerminalBotView on Github →