Deduplicating Multisets to make Finsets #
This file concerns Multiset.dedup
and List.dedup
as a way to create Finset
s.
Tags #
finite sets, finset
@[simp]
dedup on list and multiset #
toFinset s
removes duplicates from the multiset s
to produce a finset.
Equations
- s.toFinset = { val := s.dedup, nodup := ⋯ }
Instances For
@[simp]
theorem
Multiset.Nodup.toFinset_inj
{α : Type u_1}
[DecidableEq α]
{l l' : Multiset α}
(hl : l.Nodup)
(hl' : l'.Nodup)
(h : l.toFinset = l'.toFinset)
:
@[simp]
@[simp]
@[simp]
instance
Multiset.isWellFounded_ssubset
{β : Type u_2}
:
IsWellFounded (Multiset β) fun (x1 x2 : Multiset β) => x1 ⊂ x2
@[simp]
@[simp]
@[simp]
@[simp]
theorem
List.perm_of_nodup_nodup_toFinset_eq
{α : Type u_1}
[DecidableEq α]
{l l' : List α}
(hl : l.Nodup)
(hl' : l'.Nodup)
(h : l.toFinset = l'.toFinset)
:
l.Perm l'
@[simp]
@[simp]