partial finset.filter?

Stream: general

[Kenny Lau]

Currently:

finset.filter : Π {α : Type u_1} (p : α → Prop) [_inst_3 : decidable_pred p], finset α → finset α

I wonder if there's a similar function, but instead of defining p everywhere, just define it on the input finset?