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