Commit 2024-05-07 20:39 b3037511

feat: mapsTo, surjOn and injOn are preserved by Filter.map (#12385) And use it to simplify the proof of completeSpace_iff_isComplete_range. I also add the consequence of the previous result that any uniform embedding from a complete space to a hausdorff space is a closed embedding (I agree this may be a bit unrelated, but I was in the area). Notes about the filter results:

• the left/right inverse results are not used, but I think they can be helpful. I'm okay with removing them.
• the new API doesn't match very well the existing one, but after way more time that I'm willing to admit I came to the conclusion that it doesn't make sense to make it better without reorganizing and splitting the whole file.