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
Instances For
    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
    Instances For
      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
      Instances For
        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
        source
        @[simp]
        theorem Finset.perm_toList {α : Type u_1} {f₁ f₂ : Finset α} :
        f₁.toList.Perm f₂.toList ↔ f₁ = f₂
        source
        @[deprecated Finset.perm_toList (since := "2025-08-05")]
        theorem perm_toList {α : Type u_1} {f₁ f₂ : Finset α} :
        f₁.toList.Perm f₂.toList ↔ f₁ = f₂

        Alias of Finset.perm_toList.