Theorem Preorder.hasLimit_iff_hasGLB

Modification history

2025-12-01 17:54

Mathlib/CategoryTheory/Limits/Preorder.lean

feat(CategoryTheory): improve API for limits in preorders (#32178)

Modified Preorder.hasLimit_iff_hasGLB View on Github →

2025-11-01 00:46

Mathlib/CategoryTheory/Limits/Preorder.lean

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

Added Preorder.hasLimit_iff_hasGLB View on Github →