Zulip Chat Archive

Stream: Is there code for X?

Topic: nodup vs. count vs length


view this post on Zulip Jakob Scholbach (Mar 20 2021 at 20:40):

Is there a statement such as: for a multiset with nodup, the count equals the length?

view this post on Zulip Ruben Van de Velde (Mar 20 2021 at 20:44):

I don't see anything at https://leanprover-community.github.io/mathlib_docs/data/multiset/nodup.html , though I don't know what you mean by the count

view this post on Zulip Jakob Scholbach (Mar 20 2021 at 20:49):

I meant https://leanprover-community.github.io/mathlib_docs/data/multiset/basic.html#multiset.count

view this post on Zulip Yakov Pechersky (Mar 21 2021 at 00:15):

Do you mean that the sum of count should be the length? Should be a simple statement using induction on the multiset ad the existing lemmas, or by lifting the statement about lists that says that lists that are related by a perm must have the same length.

view this post on Zulip Mario Carneiro (Mar 21 2021 at 00:17):

I think this theorem exists

view this post on Zulip Mario Carneiro (Mar 21 2021 at 00:19):

If you interpret count as erase_dup.length then this is docs#multiset.erase_dup_eq_self

view this post on Zulip Mario Carneiro (Mar 21 2021 at 00:21):

The theorem Yakov is talking about is docs#multiset.to_finset_sum_count_eq


Last updated: May 07 2021 at 21:10 UTC