set.finite_mem_finset

Stream: Is there code for X?

[Marcus Rossel]

set.finite_mem_finset proves that ∀ {a} (s : finset α), finite {a | a ∈ s}.
The set I'm trying to show is finite has the form { x ∈ s | p x } though (for s : finset and p being a proposition over x).
Is there some theorem for this kind of set?

[Adam Topaz]

You can filter your S with docs#finset.filter and the prop p, and go from there

[Yakov Pechersky]

That undoubtedly requires decidability of p. I would use docs#set.finite.subset