mathlib3

220d4b89 - doc(order/filter/small_sets): fix in doc (#13648)