Mathlib.Data.Finset.Dedup

Finset.dedup_eq_self theorem

[DecidableEq α] (s : Finset α) : dedup s.1 = s.1

Full source

@[simp]
theorem dedup_eq_self [DecidableEq α] (s : Finset α) : dedup s.1 = s.1 :=
  s.2.dedup

Deduplication of Finite Set's Underlying Multiset is Identity

Informal description

For any finite set $s$ of type $\alpha$ (with decidable equality), the deduplication of the underlying multiset of $s$ is equal to the underlying multiset itself.

Multiset.toFinset definition

(s : Multiset α) : Finset α

Full source

/-- `toFinset s` removes duplicates from the multiset `s` to produce a finset. -/
def toFinset (s : Multiset α) : Finset α :=
  ⟨_, nodup_dedup s⟩

Finite set from multiset via deduplication

Informal description

The function `toFinset` takes a multiset `s` and returns the finite set obtained by removing duplicate elements from `s`.

Multiset.toFinset_val theorem

(s : Multiset α) : s.toFinset.1 = s.dedup

Full source

@[simp]
theorem toFinset_val (s : Multiset α) : s.toFinset.1 = s.dedup :=
  rfl

Equality between finite set's underlying multiset and deduplicated multiset: $\mathrm{toFinset}(s).\mathrm{val} = s.\mathrm{dedup}$

Informal description

For any multiset $s$ over a type $\alpha$, the underlying multiset of the finite set obtained by removing duplicates from $s$ is equal to the deduplicated multiset $s.\mathrm{dedup}$.

Multiset.toFinset_eq theorem

{s : Multiset α} (n : Nodup s) : Finset.mk s n = s.toFinset

Full source

theorem toFinset_eq {s : Multiset α} (n : Nodup s) : Finset.mk s n = s.toFinset :=
  Finset.val_inj.1 n.dedup.symm

Equality of Finite Set Constructions for Duplicate-Free Multisets

Informal description

For any multiset $s$ over a type $\alpha$ with no duplicate elements (i.e., $\mathrm{Nodup}\, s$ holds), the finite set constructed directly from $s$ is equal to the finite set obtained by removing duplicates from $s$ via the `toFinset` function.

Multiset.Nodup.toFinset_inj theorem

{l l' : Multiset α} (hl : Nodup l) (hl' : Nodup l') (h : l.toFinset = l'.toFinset) : l = l'

Full source

theorem Nodup.toFinset_inj {l l' : Multiset α} (hl : Nodup l) (hl' : Nodup l')
    (h : l.toFinset = l'.toFinset) : l = l' := by
  simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h

Injectivity of Finite Set Construction for Duplicate-Free Multisets

Informal description

For any duplicate-free multisets $l$ and $l'$ over a type $\alpha$, if their corresponding finite sets obtained via deduplication are equal (i.e., $\operatorname{toFinset}(l) = \operatorname{toFinset}(l')$), then the original multisets are equal ($l = l'$).

Multiset.mem_toFinset theorem

{a : α} {s : Multiset α} : a ∈ s.toFinset ↔ a ∈ s

Full source

@[simp]
theorem mem_toFinset {a : α} {s : Multiset α} : a ∈ s.toFinseta ∈ s.toFinset ↔ a ∈ s :=
  mem_dedup

Membership in Finite Set from Multiset Equals Membership in Original Multiset

Informal description

For any element $a$ and multiset $s$, the element $a$ belongs to the finite set obtained from $s$ by removing duplicates if and only if $a$ belongs to $s$.

Multiset.toFinset_subset theorem

: s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Full source

@[simp]
theorem toFinset_subset : s.toFinset ⊆ t.toFinsets.toFinset ⊆ t.toFinset ↔ s ⊆ t := by
  simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]

Subset Correspondence between Multisets and their Finite Sets

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the finite set obtained from $s$ is a subset of the finite set obtained from $t$ if and only if $s$ is a submultiset of $t$, i.e., $\operatorname{toFinset}(s) \subseteq \operatorname{toFinset}(t) \leftrightarrow s \subseteq t$.

Multiset.toFinset_ssubset theorem

: s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Full source

@[simp]
theorem toFinset_ssubset : s.toFinset ⊂ t.toFinsets.toFinset ⊂ t.toFinset ↔ s ⊂ t := by
  simp_rw [Finset.ssubset_def, toFinset_subset]
  rfl

Strict Subset Correspondence between Multisets and their Finite Sets

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the finite set obtained from $s$ is a strict subset of the finite set obtained from $t$ if and only if $s$ is a strict submultiset of $t$, i.e., $\operatorname{toFinset}(s) \subset \operatorname{toFinset}(t) \leftrightarrow s \subset t$.

Multiset.toFinset_dedup theorem

(m : Multiset α) : m.dedup.toFinset = m.toFinset

Full source

@[simp]
theorem toFinset_dedup (m : Multiset α) : m.dedup.toFinset = m.toFinset := by
  simp_rw [toFinset, dedup_idem]

Deduplication Invariance in Finite Set Conversion

Informal description

For any multiset $m$ over a type $\alpha$, the finite set obtained by first deduplicating $m$ and then converting to a finite set is equal to the finite set obtained by directly converting $m$ to a finite set, i.e., $\operatorname{toFinset}(\operatorname{dedup}(m)) = \operatorname{toFinset}(m)$.

Multiset.isWellFounded_ssubset instance

: IsWellFounded (Multiset β) (· ⊂ ·)

Full source

instance isWellFounded_ssubset : IsWellFounded (Multiset β) (· ⊂ ·) := by
  classical
  exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2

Well-foundedness of the Strict Submultiset Relation

Informal description

The strict submultiset relation $\subset$ on multisets over any type $\beta$ is well-founded. That is, every non-empty collection of multisets has a minimal element with respect to $\subset$.

Finset.val_toFinset theorem

[DecidableEq α] (s : Finset α) : s.val.toFinset = s

Full source

@[simp]
theorem val_toFinset [DecidableEq α] (s : Finset α) : s.val.toFinset = s := by
  ext
  rw [Multiset.mem_toFinset, ← mem_def]

Finite Set Invariance Under Multiset Conversion: $(\operatorname{val} s).\operatorname{toFinset} = s$

Informal description

For any finite set $s$ of type $\alpha$ (with decidable equality), the finite set obtained by converting the underlying multiset of $s$ back to a finite set is equal to $s$ itself. In other words, $(\operatorname{val} s).\operatorname{toFinset} = s$.

Finset.val_le_iff_val_subset theorem

{a : Finset α} {b : Multiset α} : a.val ≤ b ↔ a.val ⊆ b

Full source

theorem val_le_iff_val_subset {a : Finset α} {b : Multiset α} : a.val ≤ b ↔ a.val ⊆ b :=
  Multiset.le_iff_subset a.nodup

Finite Set Multiset Order vs Subset Relation: $a.val \leq b \leftrightarrow a.val \subseteq b$

Informal description

For a finite set $a$ (of type `Finset α`) and a multiset $b$ (of type `Multiset α$), the underlying multiset of $a$ is less than or equal to $b$ in the multiset order if and only if the underlying multiset of $a$ is a subset of $b$.

List.toFinset definition

(l : List α) : Finset α

Full source

/-- `toFinset l` removes duplicates from the list `l` to produce a finset. -/
def toFinset (l : List α) : Finset α :=
  Multiset.toFinset l

Finite set from list via deduplication

Informal description

The function `toFinset` takes a list `l` and returns the finite set obtained by removing duplicate elements from `l`. This is done by first converting the list to a multiset and then applying the `Multiset.toFinset` function.

List.toFinset_val theorem

(l : List α) : l.toFinset.1 = (l.dedup : Multiset α)

Full source

@[simp]
theorem toFinset_val (l : List α) : l.toFinset.1 = (l.dedup : Multiset α) :=
  rfl

Equality of Multiset Representations: $\text{val}(l.\text{toFinset}) = (l.\text{dedup} : \text{Multiset } \alpha)$

Informal description

For any list $l$ of elements of type $\alpha$, the underlying multiset of the finite set obtained from $l$ via `toFinset` is equal to the multiset obtained by removing duplicate elements from $l$ (keeping last occurrences) and then casting to a multiset. In symbols: $\text{val}(l.\text{toFinset}) = (l.\text{dedup} : \text{Multiset } \alpha)$.

List.toFinset_coe theorem

(l : List α) : (l : Multiset α).toFinset = l.toFinset

Full source

@[simp]
theorem toFinset_coe (l : List α) : (l : Multiset α).toFinset = l.toFinset :=
  rfl

Equality of Finset Constructions from List via Multiset and Direct Deduplication

Informal description

For any list $l$ of elements of type $\alpha$, the finite set obtained by first converting $l$ to a multiset and then removing duplicates is equal to the finite set obtained by directly removing duplicates from $l$. In other words, $(l : \text{Multiset } \alpha).\text{toFinset} = l.\text{toFinset}$.

List.toFinset_eq theorem

(n : Nodup l) : @Finset.mk α l n = l.toFinset

Full source

theorem toFinset_eq (n : Nodup l) : @Finset.mk α l n = l.toFinset :=
  Multiset.toFinset_eq <| by rwa [Multiset.coe_nodup]

Equality of Finset Constructions for Duplicate-Free Lists

Informal description

For any list $l$ of elements of type $\alpha$ with no duplicates (i.e., $\mathrm{Nodup}\, l$ holds), the finite set constructed directly from $l$ is equal to the finite set obtained by removing duplicates from $l$ via the `toFinset` function. In symbols: $\mathrm{Finset.mk}\, l\, n = l.\mathrm{toFinset}$.

List.mem_toFinset theorem

: a ∈ l.toFinset ↔ a ∈ l

Full source

@[simp]
theorem mem_toFinset : a ∈ l.toFinseta ∈ l.toFinset ↔ a ∈ l :=
  mem_dedup

Membership in Finite Set from List via Deduplication Equals Membership in Original List

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the element $a$ belongs to the finite set obtained by removing duplicates from $l$ if and only if $a$ belongs to the original list $l$. That is, $a \in l.\mathrm{toFinset} \leftrightarrow a \in l$.

List.coe_toFinset theorem

(l : List α) : (l.toFinset : Set α) = {a | a ∈ l}

Full source

@[simp, norm_cast]
theorem coe_toFinset (l : List α) : (l.toFinset : Set α) = { a | a ∈ l } :=
  Set.ext fun _ => List.mem_toFinset

Underlying Set of Deduplicated List Equals Set of List Elements

Informal description

For any list $l$ of elements of type $\alpha$, the underlying set of the finite set obtained by removing duplicates from $l$ is equal to the set $\{a \mid a \in l\}$ of all elements in $l$.

List.toFinset_surj_on theorem

: Set.SurjOn toFinset {l : List α | l.Nodup} Set.univ

Full source

theorem toFinset_surj_on : Set.SurjOn toFinset { l : List α | l.Nodup } Set.univ := by
  rintro ⟨⟨l⟩, hl⟩ _
  exact ⟨l, hl, (toFinset_eq hl).symm⟩

Surjectivity of `toFinset` from Duplicate-Free Lists to All Finite Sets

Informal description

The function `toFinset` is surjective from the set of duplicate-free lists to the universal set of finite sets. In other words, for every finite set $S$ of type $\alpha$, there exists a duplicate-free list $l$ such that $l.\mathrm{toFinset} = S$.

List.toFinset_surjective theorem

: Surjective (toFinset : List α → Finset α)

Full source

theorem toFinset_surjective : Surjective (toFinset : List α → Finset α) := fun s =>
  let ⟨l, _, hls⟩ := toFinset_surj_on (Set.mem_univ s)
  ⟨l, hls⟩

Surjectivity of List-to-Finset Conversion

Informal description

The function `toFinset` from lists to finite sets is surjective. That is, for every finite set $S$ of type $\alpha$, there exists a list $l$ of elements of type $\alpha$ such that $l.\text{toFinset} = S$.

List.toFinset_eq_iff_perm_dedup theorem

: l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup

Full source

theorem toFinset_eq_iff_perm_dedup : l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup := by
  simp [Finset.ext_iff, perm_ext_iff_of_nodup (nodup_dedup _) (nodup_dedup _)]

Equality of Finite Sets via Permutation of Deduplicated Lists

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, the finite sets obtained by removing duplicates from $l$ and $l'$ are equal if and only if the deduplicated versions of $l$ and $l'$ are permutations of each other. That is, $l.\text{toFinset} = l'.\text{toFinset} \leftrightarrow \text{dedup}(l) \sim \text{dedup}(l')$, where $\sim$ denotes permutation equivalence.

List.toFinset.ext_iff theorem

{a b : List α} : a.toFinset = b.toFinset ↔ ∀ x, x ∈ a ↔ x ∈ b

Full source

theorem toFinset.ext_iff {a b : List α} : a.toFinset = b.toFinset ↔ ∀ x, x ∈ a ↔ x ∈ b := by
  simp only [Finset.ext_iff, mem_toFinset]

Equality of Deduplicated Finite Sets via Element Membership

Informal description

For any two lists $a$ and $b$ of elements of type $\alpha$, the finite sets obtained by removing duplicates from $a$ and $b$ are equal if and only if every element $x$ belongs to $a$ exactly when it belongs to $b$. In other words, $a.\text{toFinset} = b.\text{toFinset} \leftrightarrow (\forall x, x \in a \leftrightarrow x \in b)$.

List.toFinset.ext theorem

: (∀ x, x ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset

Full source

theorem toFinset.ext : (∀ x, x ∈ lx ∈ l ↔ x ∈ l') → l.toFinset = l'.toFinset :=
  toFinset.ext_iff.mpr

Equality of Deduplicated Finite Sets via Element Membership Condition

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, if every element $x$ belongs to $l$ if and only if it belongs to $l'$, then the finite sets obtained by removing duplicates from $l$ and $l'$ are equal, i.e., $l.\text{toFinset} = l'.\text{toFinset}$.

List.toFinset_eq_of_perm theorem

(l l' : List α) (h : l ~ l') : l.toFinset = l'.toFinset

Full source

theorem toFinset_eq_of_perm (l l' : List α) (h : l ~ l') : l.toFinset = l'.toFinset :=
  toFinset_eq_iff_perm_dedup.mpr h.dedup

Permutation Preserves Finite Set Equality

Informal description

For any two lists $l$ and $l'$ of elements of type $\alpha$, if $l$ is a permutation of $l'$, then the finite sets obtained by removing duplicates from $l$ and $l'$ are equal, i.e., $l.\text{toFinset} = l'.\text{toFinset}$.

List.perm_of_nodup_nodup_toFinset_eq theorem

(hl : Nodup l) (hl' : Nodup l') (h : l.toFinset = l'.toFinset) : l ~ l'

Full source

theorem perm_of_nodup_nodup_toFinset_eq (hl : Nodup l) (hl' : Nodup l')
    (h : l.toFinset = l'.toFinset) : l ~ l' := by
  rw [← Multiset.coe_eq_coe]
  exact Multiset.Nodup.toFinset_inj hl hl' h

Permutation of Duplicate-Free Lists with Equal Finite Sets

Informal description

For any two duplicate-free lists $l$ and $l'$ of elements of type $\alpha$, if their corresponding finite sets obtained by removing duplicates are equal (i.e., $l.\text{toFinset} = l'.\text{toFinset}$), then $l$ is a permutation of $l'$.

List.toFinset_reverse theorem

{l : List α} : toFinset l.reverse = l.toFinset

Full source

@[simp]
theorem toFinset_reverse {l : List α} : toFinset l.reverse = l.toFinset :=
  toFinset_eq_of_perm _ _ (reverse_perm l)

Finite Set Equality under List Reversal: $l.\text{reverse}.\text{toFinset} = l.\text{toFinset}$

Informal description

For any list $l$ of elements of type $\alpha$, the finite set obtained by removing duplicates from the reversed list $l.\text{reverse}$ is equal to the finite set obtained by removing duplicates from $l$, i.e., $l.\text{reverse}.\text{toFinset} = l.\text{toFinset}$.

Finset.toList definition

(s : Finset α) : List α

Full source

/-- Produce a list of the elements in the finite set using choice. -/
noncomputable def toList (s : Finset α) : List α :=
  s.1.toList

List representation of a finite set

Informal description

Given a finite set $s$ over a type $\alpha$, the function returns a list containing all elements of $s$ (without duplicates), where the order of elements is determined by the choice function.

Finset.nodup_toList theorem

(s : Finset α) : s.toList.Nodup

Full source

theorem nodup_toList (s : Finset α) : s.toList.Nodup := by
  rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]
  exact s.nodup

No Duplicates in List Representation of Finite Set

Informal description

For any finite set $s$ over a type $\alpha$, the list representation of $s$ (obtained via `toList`) contains no duplicate elements.

Finset.mem_toList theorem

{a : α} {s : Finset α} : a ∈ s.toList ↔ a ∈ s

Full source

@[simp]
theorem mem_toList {a : α} {s : Finset α} : a ∈ s.toLista ∈ s.toList ↔ a ∈ s :=
  Multiset.mem_toList

Membership Equivalence Between Finite Set and Its List Representation

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of type $\alpha$, the element $a$ belongs to the list representation of $s$ if and only if $a$ belongs to $s$. That is, $a \in \text{toList}(s) \leftrightarrow a \in s$.

Finset.coe_toList theorem

(s : Finset α) : (s.toList : Multiset α) = s.val

Full source

@[simp, norm_cast]
theorem coe_toList (s : Finset α) : (s.toList : Multiset α) = s.val :=
  s.val.coe_toList

Equality of Multiset Coercion and Underlying Value for Finite Sets

Informal description

For any finite set $s$ over a type $\alpha$, the multiset obtained by coercing the list representation of $s$ (via `toList`) is equal to the underlying multiset value of $s$. That is, $\text{toList}(s) = s.\text{val}$ where the left side is interpreted as a multiset.

Finset.toList_toFinset theorem

[DecidableEq α] (s : Finset α) : s.toList.toFinset = s

Full source

@[simp]
theorem toList_toFinset [DecidableEq α] (s : Finset α) : s.toList.toFinset = s := by
  ext
  simp

Finite Set to List to Finite Set Roundtrip Identity

Informal description

For any finite set $s$ over a type $\alpha$ with decidable equality, converting $s$ to a list and then back to a finite set yields the original set $s$. That is, $\text{toFinset}(\text{toList}(s)) = s$.

List.toFinset_toList theorem

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

Full source

theorem _root_.List.toFinset_toList [DecidableEq α] {s : List α} (hs : s.Nodup) :
    s.toFinset.toList.Perm s := by
  apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs
  rw [toList_toFinset]

Permutation Preservation in List-Finset Conversion for Duplicate-Free Lists

Informal description

For any duplicate-free list $s$ of elements of type $\alpha$ with decidable equality, the list obtained by converting $s$ to a finite set and then back to a list is a permutation of the original list $s$. That is, $\text{toList}(\text{toFinset}(s)) \sim s$.

Finset.exists_list_nodup_eq theorem

[DecidableEq α] (s : Finset α) : ∃ l : List α, l.Nodup ∧ l.toFinset = s

Full source

theorem exists_list_nodup_eq [DecidableEq α] (s : Finset α) :
    ∃ l : List α, l.Nodup ∧ l.toFinset = s :=
  ⟨s.toList, s.nodup_toList, s.toList_toFinset⟩

Existence of Duplicate-Free List Representing Finite Set

Informal description

For any finite set $s$ over a type $\alpha$ with decidable equality, there exists a list $l$ of elements of $\alpha$ without duplicates such that the finite set obtained from $l$ by removing duplicates is equal to $s$. That is, there exists $l$ such that $l$ has no duplicates and $\text{toFinset}(l) = s$.

Tags