mathlib3

394dec32 - feat(order/filter/small_sets): define the filter of small sets (#13467)

feat(order/filter/small_sets): define the filter of small sets (#13467) * Main author is @PatrickMassot * From the sphere eversion project * Required for convolutions Co-authored by: Patrick Massot <patrick.massot@u-psud.fr>