## Stream: general

### Topic: Make multiset.powerset nodup

#### Yaël Dillies (Oct 26 2021 at 12:44):

I was expecting docs#multiset.powerset to be nodup already, but it's not. I want the result that m.powerset.card is the product of the multiplicities of elements of m + 1:

import algebra.big_operators.basic

open_locale big_operators

-- currently wrong but I want it to be right
lemma multiset.card_powerset' {α : Type*} [decidable_eq α] (s : multiset α) :
s.powerset.card = ∏ x in s.to_finset, (s.count x + 1) :=
sorry

lemma multiset.card_powerset_to_finset {α : Type*} [decidable_eq α] (s : multiset α) :
s.powerset.to_finset.card = ∏ x in s.to_finset, (s.count x + 1) :=
sorry


Which of the above ways should be the correct spelling?

#### Johan Commelin (Oct 26 2021 at 12:45):

I think multiset.powerset is deliberately not nodup.

#### Yaël Dillies (Oct 26 2021 at 12:46):

What's the motivation?

#### Johan Commelin (Oct 26 2021 at 12:46):

@Mario Carneiro :up:

#### Mario Carneiro (Oct 26 2021 at 12:47):

it doesn't depend on equality at all, it's a pure multiset operation

#### Yaël Dillies (Oct 26 2021 at 12:48):

Ah, because grinding it through multiset.to_finset would require decidable equality :sad:

#### Mario Carneiro (Oct 26 2021 at 12:48):

If you want to nodup it first, then why not use s.to_finset.powerset?

#### Yaël Dillies (Oct 26 2021 at 12:48):

Ah no that's not what I want!

#### Yaël Dillies (Oct 26 2021 at 12:49):

s.powerset.to_finset does, however.

#### Yaël Dillies (Oct 26 2021 at 12:49):

I'm trying to define locally_finite_order (multiset α).

#### Mario Carneiro (Oct 26 2021 at 12:50):

I rather prefer the theorem s.powerset.card = 2 ^ s.card

#### Yaël Dillies (Oct 26 2021 at 12:50):

Yeah, and I assume it makes docs#finset.card_powerset quite direct.

#### Yakov Pechersky (Oct 26 2021 at 13:45):

multiset.powerset is choosing from a bag without replacement. why would it be nodup?

Last updated: Aug 03 2023 at 10:10 UTC