Deduplicating Multisets to make Finsets

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

Tags

finite sets, finset

@[simp]

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

dedup on list and multiset

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

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

@[simp]

theorem Multiset.toFinset_val {α : Type u_1} [DecidableEq α] (s : Multiset α) : s.toFinset.val = s.dedup

theorem Multiset.toFinset_eq {α : Type u_1} [DecidableEq α] {s : Multiset α} (n : s.Nodup) : { val := s, nodup := n } = s.toFinset

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'

@[simp]

theorem Multiset.mem_toFinset {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s.toFinset ↔ a ∈ s

@[simp]

theorem Multiset.toFinset_subset {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s.toFinset ⊆ t.toFinset ↔ s ⊆ t

@[simp]

theorem Multiset.toFinset_ssubset {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s.toFinset ⊂ t.toFinset ↔ s ⊂ t

@[simp]

theorem Multiset.toFinset_dedup {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.dedup.toFinset = m.toFinset

instance Multiset.isWellFounded_ssubset {β : Type u_2} : IsWellFounded (Multiset β) fun (x1 x2 : Multiset β) => x1 ⊂ x2

@[simp]

theorem Finset.val_toFinset {α : Type u_1} [DecidableEq α] (s : Finset α) : s.val.toFinset = s

theorem Finset.val_le_iff_val_subset {α : Type u_1} {a : Finset α} {b : Multiset α} : a.val ≤ b ↔ a.val ⊆ b

def List.toFinset {α : Type u_1} [DecidableEq α] (l : List α) : Finset α

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

@[simp]

theorem List.toFinset_val {α : Type u_1} [DecidableEq α] (l : List α) : l.toFinset.val = ↑l.dedup

@[simp]

theorem List.toFinset_coe {α : Type u_1} [DecidableEq α] (l : List α) : (↑l).toFinset = l.toFinset

theorem List.toFinset_eq {α : Type u_1} [DecidableEq α] {l : List α} (n : l.Nodup) : { val := ↑l, nodup := n } = l.toFinset

@[simp]

theorem List.mem_toFinset {α : Type u_1} [DecidableEq α] {l : List α} {a : α} : a ∈ l.toFinset ↔ a ∈ l

@[simp]

theorem List.coe_toFinset {α : Type u_1} [DecidableEq α] (l : List α) : ↑l.toFinset = {a : α | a ∈ l}

theorem List.toFinset_surj_on {α : Type u_1} [DecidableEq α] : Set.SurjOn toFinset {l : List α | l.Nodup} Set.univ

theorem List.toFinset_surjective {α : Type u_1} [DecidableEq α] : Function.Surjective toFinset

theorem List.toFinset_eq_iff_perm_dedup {α : Type u_1} [DecidableEq α] {l l' : List α} : l.toFinset = l'.toFinset ↔ l.dedup.Perm l'.dedup

theorem List.toFinset.ext_iff {α : Type u_1} [DecidableEq α] {a b : List α} : a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b

theorem List.toFinset.ext {α : Type u_1} [DecidableEq α] {l l' : List α} : (∀ (x : α), x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset

theorem List.toFinset_eq_of_perm {α : Type u_1} [DecidableEq α] (l l' : List α) (h : l.Perm l') : l.toFinset = l'.toFinset

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]

theorem List.toFinset_reverse {α : Type u_1} [DecidableEq α] {l : List α} : l.reverse.toFinset = l.toFinset

noncomputable def Finset.toList {α : Type u_1} (s : Finset α) : List α

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

theorem Finset.nodup_toList {α : Type u_1} (s : Finset α) : s.toList.Nodup

@[simp]

theorem Finset.mem_toList {α : Type u_1} {a : α} {s : Finset α} : a ∈ s.toList ↔ a ∈ s

@[simp]

theorem Finset.coe_toList {α : Type u_1} (s : Finset α) : ↑s.toList = s.val

@[simp]

theorem Finset.toList_toFinset {α : Type u_1} [DecidableEq α] (s : Finset α) : s.toList.toFinset = s

theorem List.toFinset_toList {α : Type u_1} [DecidableEq α] {s : List α} (hs : s.Nodup) : s.toFinset.toList.Perm s

theorem Finset.exists_list_nodup_eq {α : Type u_1} [DecidableEq α] (s : Finset α) : ∃ (l : List α), l.Nodup ∧ l.toFinset = s

@[simp]

theorem Finset.perm_toList {α : Type u_1} {f₁ f₂ : Finset α} : f₁.toList.Perm f₂.toList ↔ f₁ = f₂