Zulip Chat Archive

Is there some way to define a function recursively over a finset, where each "iteration" has access to one element of the set?
First I thought this shouldn't be possible, since choosing an element from a set isn't really possible. But then again there's classical.choice.

I want to do something for each element in a finset and so far my approach has been to sort the set into a list first, which requires some kind of order on the elements though.

So far I've only found finset.strong_induction_on, which doesn't suit my case (I think).

Alex J. Best (Jan 12 2021 at 14:37):

Maybe docs#finset.induction_on'

Logan Murphy (Jan 12 2021 at 14:37):

I haven't done a ton of this kind of stuff with finset, but maybe you can do the recursion on the underlying multiset (lists up to permutation) and then provide a proof that your function doesn't introduce duplicates

Marcus Rossel (Jan 12 2021 at 14:40):

Perhaps I should clarify my exact use case:
I have some object o : O and p : finset P. For each x ∈ p I need to update something about o by using p. I happen to know that the order in which the xs are chosen doesn't matter.