Def BoundedOrder.ofUnique

Modification history

2026-05-25 09:15
Mathlib/Order/BoundedOrder/Basic.lean
feat: cofinal subset of regular cardinal is isomorphic to it (#38362) …
Added BoundedOrder.ofUniqueView on Github →