Documentation

Mathlib.Data.Finset.Dedup

Deduplicating Multisets to make Finsets #

This file concerns Multiset.dedup and List.dedup as a way to create Finsets.

Tags #

finite sets, finset

source
@[simp]
theorem Finset.dedup_eq_self {α : Type u_1} [DecidableEq α] (s : Finset α) :
s.val.dedup = s.val

dedup on list and multiset #

source
def Multiset.toFinset {α : Type u_1} [DecidableEq α] (s : Multiset α) :
Finset α

toFinset s removes duplicates from the multiset s to produce a finset.

Equations
source
@[simp]
theorem Multiset.toFinset_val {α : Type u_1} [DecidableEq α] (s : Multiset α) :
s.toFinset.val = s.dedup
source
theorem Multiset.toFinset_eq {α : Type u_1} [DecidableEq α] {s : Multiset α} (n : s.Nodup) :
{ val := s, nodup := n } = s.toFinset
source
theorem Multiset.Nodup.toFinset_inj {α : Type u_1} [DecidableEq α] {l l' : Multiset α} (hl : l.Nodup) (hl' : l'.Nodup) (h : l.toFinset = l'.toFinset) :
l = l'
source
@[simp]
theorem Multiset.mem_toFinset {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
a ∈ s.toFinset ↔ a ∈ s
source
@[simp]
theorem Multiset.toFinset_subset {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
s.toFinset ⊆ t.toFinset ↔ s ⊆ t
source
@[simp]
theorem Multiset.toFinset_ssubset {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
s.toFinset ⊂ t.toFinset ↔ s ⊂ t
source
@[simp]
theorem Multiset.toFinset_dedup {α : Type u_1} [DecidableEq α] (m : Multiset α) :
m.dedup.toFinset = m.toFinset
source
instance Multiset.isWellFounded_ssubset {β : Type u_2} :
IsWellFounded (Multiset β) fun (x1 x2 : Multiset β) => x1 ⊂ x2
source
@[simp]
theorem Finset.val_toFinset {α : Type u_1} [DecidableEq α] (s : Finset α) :
s.val.toFinset = s
source
theorem Finset.val_le_iff_val_subset {α : Type u_1} {a : Finset α} {b : Multiset α} :
a.val ≤ b ↔ a.val ⊆ b
source
def List.toFinset {α : Type u_1} [DecidableEq α] (l : List α) :
Finset α

toFinset l removes duplicates from the list l to produce a finset.

Equations
source
@[simp]
theorem List.toFinset_val {α : Type u_1} [DecidableEq α] (l : List α) :
l.toFinset.val = ↑l.dedup
source
@[simp]
theorem List.toFinset_coe {α : Type u_1} [DecidableEq α] (l : List α) :
(↑l).toFinset = l.toFinset
source
theorem List.toFinset_eq {α : Type u_1} [DecidableEq α] {l : List α} (n : l.Nodup) :
{ val := ↑l, nodup := n } = l.toFinset
source
@[simp]
theorem List.mem_toFinset {α : Type u_1} [DecidableEq α] {l : List α} {a : α} :
a ∈ l.toFinset ↔ a ∈ l
source
@[simp]
theorem List.coe_toFinset {α : Type u_1} [DecidableEq α] (l : List α) :
↑l.toFinset = {a : α | a ∈ l}
source
theorem List.toFinset_surj_on {α : Type u_1} [DecidableEq α] :
Set.SurjOn toFinset {l : List α | l.Nodup} Set.univ
source
theorem List.toFinset_surjective {α : Type u_1} [DecidableEq α] :
Function.Surjective toFinset
source
theorem List.toFinset_eq_iff_perm_dedup {α : Type u_1} [DecidableEq α] {l l' : List α} :
l.toFinset = l'.toFinset ↔ l.dedup.Perm l'.dedup
source
theorem List.toFinset.ext_iff {α : Type u_1} [DecidableEq α] {a b : List α} :
a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
source
theorem List.toFinset.ext {α : Type u_1} [DecidableEq α] {l l' : List α} :
(∀ (x : α), x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset
source
theorem List.toFinset_eq_of_perm {α : Type u_1} [DecidableEq α] (l l' : List α) (h : l.Perm l') :
l.toFinset = l'.toFinset
source
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'
source
@[simp]
theorem List.toFinset_reverse {α : Type u_1} [DecidableEq α] {l : List α} :
l.reverse.toFinset = l.toFinset
source
noncomputable def Finset.toList {α : Type u_1} (s : Finset α) :
List α

Produce a list of the elements in the finite set using choice.

Equations
source
theorem Finset.nodup_toList {α : Type u_1} (s : Finset α) :
s.toList.Nodup
source
@[simp]
theorem Finset.mem_toList {α : Type u_1} {a : α} {s : Finset α} :
a ∈ s.toList ↔ a ∈ s
source
@[simp]
theorem Finset.coe_toList {α : Type u_1} (s : Finset α) :
↑s.toList = s.val
source
@[simp]
theorem Finset.toList_toFinset {α : Type u_1} [DecidableEq α] (s : Finset α) :
s.toList.toFinset = s
source
theorem List.toFinset_toList {α : Type u_1} [DecidableEq α] {s : List α} (hs : s.Nodup) :
s.toFinset.toList.Perm s
source
theorem Finset.exists_list_nodup_eq {α : Type u_1} [DecidableEq α] (s : Finset α) :
∃ (l : List α), l.Nodup ∧ l.toFinset = s