Stream: new members
Topic: finset minus set
Iocta (Mar 20 2021 at 22:28):
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ᶜ
Hanting Zhang (Mar 20 2021 at 22:36):
Have you looked through the
finset docs? Set differences are called
Iocta (Mar 20 2021 at 22:38):
That only works on finsets
Hanting Zhang (Mar 20 2021 at 22:39):
Ah, my bad, I misread.
Adam Topaz (Mar 20 2021 at 22:46):
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 (Mar 20 2021 at 22:49):
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.
Last updated: May 08 2021 at 10:12 UTC