Commit 2026-03-18 12:31 b459ce1c

View on Github →

feat: IsCofinal s implies IsCofinal (f '' s) (#36715)

Estimated changes

Modified Mathlib/Order/Cofinal.lean

added theorem GaloisConnection.isCofinal_range

deleted theorem GaloisConnection.map_cofinal

added theorem GaloisConnection.map_isCofinal

added theorem IsCofinal.image

deleted theorem OrderIso.map_cofinal

added theorem OrderIso.map_isCofinal

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean