mathlib3

9600f4f6 - feat(order/filter/bases): view a filter as a *bundled* filter basis (#14506)

feat(order/filter/bases): view a filter as a *bundled* filter basis (#14506) We already have `filter.basis_sets` which says that the elements of a filter are a basis of itself (in the `has_basis` sense), but we don't have the fact that they form a filter basis (in the `filter_basis` sense), and `x ∈ f.basis_sets.is_basis.filter_basis` is not defeq to `x ∈ f`