intersection of a set and a finset as a finset

Stream: Is there code for X?

[Eric Rodriguez]

Title; this would be mighty helpful if it exists!

[Adam Topaz]

You can use docs#finset.filter

[Eric Rodriguez]

often when I use filter it ends up being awkward, but I guess that'll work fine for this tbh

[Adam Topaz]

The lemma docs#finset.mem_filter should make this a useful enough approach, I think.

[Bryan Gin-ge Chen]

Does using finset.filter count as breaking through the barrier of the set API?

[Adam Topaz]

If you use set membership as the prop, then I think it's okay?

[Yakov Pechersky]

This relies on the decidability of membership in the set, iirc