Commit 2024-05-26 15:54 c7256b5b

feat: exhibit lower adjoint for smallSets, use it to prove a better comap_smallSets (#12111) And use the new version to hide Filter.lift' where comap_smallSets was used. I was writing an exercise about Filter.smallSets and noticed we didn't have this in Mathlib. So of course I had to formalize it to check, and I think it makes the API nicer.