Stream: Is there code for X?
Topic: nodup vs. count vs length
Jakob Scholbach (Mar 20 2021 at 20:40):
Is there a statement such as: for a multiset with
count equals the length?
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
Jakob Scholbach (Mar 20 2021 at 20:49):
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.
Mario Carneiro (Mar 21 2021 at 00:17):
I think this theorem exists
Mario Carneiro (Mar 21 2021 at 00:19):
If you interpret
erase_dup.length then this is docs#multiset.erase_dup_eq_self
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