Intersection of a Finset and a Set as a Finset?

Stream: Is there code for X?

[Michael Stoll]

Is there a simple way to obtain the intersection of s : Finset α and t : Set α as a Finset α? Loogling for Finset, Set, "inter" does not produce anything close.

[Yaël Dillies]

s.filter (· ∈ t)

[Michael Stoll]

... not so easily discoverable if you think of intersections ...

[Yaël Dillies]

Feel free to add this use case to the docstring of docs#Finset.filter !

[Kyle Miller]

I think might also be able to do Set.toFinset (s \cap t)

[Michael Stoll]

I'll try to remember that. BTW, s.filter t also works (given [DecidablePred t]), but I guess this is defeq abuse...

[Kyle Miller]

(Yeah, that's defeq abuse)

[Michael Stoll]

Kyle Miller said:

I think might also be able to do Set.toFinset (s \cap t)

failed to synthesize instance Fintype ↑(↑s ∩ t)

[Kyle Miller]

The correct phrasing of DecidablePred t is DecidablePred (· ∈ t) by the way

[Michael Stoll]

I know, but to get s.filter t to work, DecidablePred (· ∈ t)does not cut it.

[Yaël Dillies]

Yes, because that's defeq abuse, as you pointed out.

[Kyle Miller]

Michael Stoll said:

failed to synthesize instance Fintype ↑(↑s ∩ t)

Set.toFinset doesn't let you avoid decidability unfortunately. This works:

import Mathlib.Data.Set.Finite

variable {α : Type*} (s : Finset α) (t : Set α) [DecidablePred (· ∈ t)]

#check Set.toFinset (s ∩ t)

[Michael Stoll]

I'll go with the filter version for now and see how I get along with that.

[Kyle Miller]

One way you can find out what you're missing is to do

import Mathlib.Data.Set.Finite

variable {α : Type*} (s : Finset α) (t : Set α)

open scoped Classical

#check Set.toFinset (s ∩ t)

and poke around the term until you find a Classical instance.

[Michael Stoll]

[DecidablePred (· ∈ t)] is needed for the s.filter version as well, so it is perhaps easy to guess in this case.

[Eric Wieser]

Yaël Dillies said:

Feel free to add this use case to the docstring of docs#Finset.filter !

#9239