mathlib

78f647f8 - chore(order/filter, topology/algebra): golf (#18097)