Theorem Filter.bind_smallSets_gc

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.bind_smallSets_gcView on Github →