finset minus set

Stream: new members

[Iocta]

How can I subtract a set from a finset and get a finset?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory

def finsub  (t : finset ℤ) (s : set ℤ) : finset ℤ := t ∩ sᶜ

doesn't work

[Hanting Zhang]

Have you looked through the finset docs? Set differences are called sdiff.

[Iocta]

That only works on finsets

[Hanting Zhang]

Ah, my bad, I misread.

[Adam Topaz]

You can use docs#finset.filter and filter out the stuff that's not in the set. I don't know if there is a better way.

[Hanting Zhang]

You could also work with sets and use set.finite. Do whatever you need in set, and then at the very end when you need a finset, use docs#set.finite.to_finset.