Theorem isCofinal_setOf_imp_lt

Modification history

2026-07-17 09:57

Mathlib/Order/Cofinal.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Deleted isCofinal_setOf_imp_lt View on Github →

2024-12-07 13:24

Mathlib/Order/Cofinal.lean

feat(Order/Cofinal): more lemmas on cofinal sets (#19680)

Added isCofinal_setOf_imp_lt View on Github →