Commit 2024-11-14 00:39 9d745bb9

View on Github →

feat(Order/Cofinal): predicate for cofinal sets (#18214) The plan is of course to redefine Order.cof as the least cardinality of a Cofinal set.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Bounds/Defs.lean

added def IsCofinal

Created Mathlib/Order/Cofinal.lean

added theorem BddAbove.of_not_isCofinal

added theorem IsCofinal.mem_of_isMax

added theorem IsCofinal.mono

added theorem IsCofinal.of_isEmpty

added theorem IsCofinal.of_not_bddAbove

added theorem IsCofinal.singleton_top

added theorem IsCofinal.top_mem

added theorem IsCofinal.trans

added theorem IsCofinal.univ

added theorem isCofinal_empty_iff

added theorem isCofinal_iff_top_mem

added theorem not_bddAbove_iff_isCofinal

added theorem not_isCofinal_iff

added theorem not_isCofinal_iff_bddAbove