Theorem Filter.smallSets_comap_eq_comap_image

Modification history

2024-05-26 15:54
Mathlib/Order/Filter/SmallSets.lean
feat: exhibit lower adjoint for smallSets, use it to prove a better comap_smallSets (#12111) …
Added Filter.smallSets_comap_eq_comap_imageView on Github →