Zulip Chat Archive

Stream: new members

Topic: multiset question


Amelia Livingston (Mar 14 2019 at 18:46):

Hi! I got stuck doing this; can anyone help? Thanks!

import data.finset

variables (α : Type*) [decidable_eq α]

example (m : multiset α) : m.to_finset =   m = 0 := sorry

Kevin Buzzard (Mar 14 2019 at 18:52):

I have so far failed twice :-)

Amelia Livingston (Mar 14 2019 at 18:53):

Ah, this works, but it's kind of long

example (β: Type u) [decidable_eq β] (m : multiset β) : m.to_finset =   m = 0 :=
begin
  rw [multiset.to_finset, finset.val_inj],
  intro H,
  change erase_dup m =  at H,
  apply eq_zero_of_forall_not_mem,
  intro x,
  assume H',
  rw [mem_erase_dup, H] at H',
  exact absurd H' (not_mem_empty x),
end

Kevin Buzzard (Mar 14 2019 at 18:54):

Looking at it now I'm wondering if it should be in the library

Kevin Buzzard (Mar 14 2019 at 18:59):

import data.finset

variables (α : Type*) [decidable_eq α]

example (m : multiset α) (h : m.to_finset = ) : m = 0 :=
begin
  apply multiset.eq_zero_of_forall_not_mem,
  rw finset.eq_empty_iff_forall_not_mem at h,
  intros x hx,
  rw multiset.mem_to_finset at hx,
  exact h x hx,
end

Maybe this is a bit better

Kenny Lau (Mar 14 2019 at 19:04):

import data.finset

variables (α : Type*) [decidable_eq α]

example (m : multiset α) : m.to_finset =   m = 0 :=
multiset.induction_on m (λ _, rfl) (λ _ _ _ H, absurd H $ by simp)

Amelia Livingston (Mar 14 2019 at 19:09):

thank you :D

Mario Carneiro (Mar 15 2019 at 09:18):

Ah, yes there is a missing library function

namespace multiset
theorem erase_dup_eq_zero {s : multiset α} : erase_dup s = 0  s = 0 :=
⟨λ h, eq_zero_of_subset_zero $ h  subset_erase_dup _,
 λ h, h.symm  erase_dup_zero
end multiset

example (m : multiset α) (h : m.to_finset = ) : m = 0 :=
multiset.erase_dup_eq_zero.1 (finset.val_inj.2 h)

Mario Carneiro (Mar 15 2019 at 09:20):

well, this theorem itself is also a missing library function

theorem to_finset_eq_empty {m : multiset α} : m.to_finset =   m = 0 :=
finset.val_inj.symm.trans multiset.erase_dup_eq_zero

Last updated: Dec 20 2023 at 11:08 UTC