Theorem GaloisConnection.map_cofinal

Modification history

2026-03-18 12:31
Mathlib/Order/Cofinal.lean
feat: `IsCofinal s` implies `IsCofinal (f '' s)` (#36715)
Deleted GaloisConnection.map_cofinalView on Github →
2024-12-07 13:24
Mathlib/Order/Cofinal.lean
feat(Order/Cofinal): more lemmas on cofinal sets (#19680)
Added GaloisConnection.map_cofinalView on Github →