Zulip Chat Archive

Stream: new members

Topic: finset minus set


view this post on Zulip 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

doesn't work

view this post on Zulip Hanting Zhang (Mar 20 2021 at 22:36):

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

view this post on Zulip Iocta (Mar 20 2021 at 22:38):

That only works on finsets

view this post on Zulip Hanting Zhang (Mar 20 2021 at 22:39):

Ah, my bad, I misread.

view this post on Zulip 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.

view this post on Zulip 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