Make multiset.powerset nodup

Stream: general

[Yaël Dillies]

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]

I think multiset.powerset is deliberately not nodup.

[Yaël Dillies]

What's the motivation?

[Johan Commelin]

@Mario Carneiro :up:

[Mario Carneiro]

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

[Yaël Dillies]

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

[Mario Carneiro]

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

[Yaël Dillies]

Ah no that's not what I want!

[Yaël Dillies]

s.powerset.to_finset does, however.

[Yaël Dillies]

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

[Mario Carneiro]

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

[Yaël Dillies]

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

[Yakov Pechersky]

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