Commit 2024-12-07 13:24 410afe3f

View on Github →

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

Estimated changes

Modified Mathlib/Order/Cofinal.lean

added theorem GaloisConnection.map_cofinal

added theorem OrderIso.map_cofinal

added theorem isCofinal_setOf_imp_lt