doc-next-gen

Mathlib.Data.Fintype.Sets

Module docstring

{"# Subsets of finite types

In a Fintype, all Sets are automatically Finsets, and there are only finitely many of them.

Main results

  • Set.toFinset: convert a subset of a finite type to a Finset
  • Finset.fintypeCoeSort: ((s : Finset α) : Type*) is a finite type
  • Fintype.finsetEquivSet: Finset α and Set α are equivalent if α is a Fintype ","### Fintype (s : Finset α) "}
Set.toFinset definition
(s : Set α) [Fintype s] : Finset α
Full source 
/-- Construct a finset enumerating a set `s`, given a `Fintype` instance. -/
def toFinset (s : Set α) [Fintype s] : Finset α :=
  (@Finset.univ s _).map <| Function.Embedding.subtype _
Conversion from a set to a finite set in a finite type
Informal description
Given a set $s$ over a finite type $\alpha$ (with a `Fintype` instance for $s$), the function `Set.toFinset` constructs a finite set (a `Finset`) that enumerates all elements of $s$. This is done by first taking the universal finite set of the subtype corresponding to $s$ and then mapping it back to $\alpha$ via the subtype inclusion embedding.
Set.toFinset_congr theorem
{s t : Set α} [Fintype s] [Fintype t] (h : s = t) : toFinset s = toFinset t
Full source 
@[congr]
theorem toFinset_congr {s t : Set α} [Fintype s] [Fintype t] (h : s = t) :
    toFinset s = toFinset t := by subst h; congr!
Equality of Finite Sets under Set Equality
Informal description
For any two sets $s$ and $t$ over a finite type $\alpha$, if $s = t$ and both sets have finite type instances, then their corresponding finite sets (via `Set.toFinset`) are equal, i.e., $\mathrm{toFinset}\, s = \mathrm{toFinset}\, t$.
Set.mem_toFinset theorem
{s : Set α} [Fintype s] {a : α} : a ∈ s.toFinset ↔ a ∈ s
Full source 
@[simp]
theorem mem_toFinset {s : Set α} [Fintype s] {a : α} : a ∈ s.toFinseta ∈ s.toFinset ↔ a ∈ s := by
  simp [toFinset]
Membership Equivalence between Set and its Finite Set Representation
Informal description
For any set $s$ over a finite type $\alpha$ with a `Fintype` instance, and for any element $a \in \alpha$, the element $a$ belongs to the finite set `s.toFinset` if and only if $a$ belongs to the set $s$.
Set.toFinset_ofFinset theorem
{p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : @Set.toFinset _ p (Fintype.ofFinset s H) = s
Full source 
/-- Many `Fintype` instances for sets are defined using an extensionally equal `Finset`.
Rewriting `s.toFinset` with `Set.toFinset_ofFinset` replaces the term with such a `Finset`. -/
theorem toFinset_ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ sx ∈ s ↔ x ∈ p) :
    @Set.toFinset _ p (Fintype.ofFinset s H) = s :=
  Finset.ext fun x => by rw [@mem_toFinset _ _ (id _), H]
Equality of Finite Set Representation with Given Finset
Informal description
For any set $p$ over a type $\alpha$ and a finite set $s$ of elements of $\alpha$ such that for all $x \in \alpha$, $x \in s$ if and only if $x \in p$, the finite set representation of $p$ (via `Set.toFinset`) is equal to $s$ when $p$ is endowed with the finite type structure derived from $s$ and $H$.
Set.decidableMemOfFintype definition
[DecidableEq α] (s : Set α) [Fintype s] (a) : Decidable (a ∈ s)
Full source 
/-- Membership of a set with a `Fintype` instance is decidable.

Using this as an instance leads to potential loops with `Subtype.fintype` under certain decidability
assumptions, so it should only be declared a local instance. -/
def decidableMemOfFintype [DecidableEq α] (s : Set α) [Fintype s] (a) : Decidable (a ∈ s) :=
  decidable_of_iff _ mem_toFinset
Decidability of membership in finite sets
Informal description
Given a type $\alpha$ with decidable equality and a set $s \subseteq \alpha$ that has a finite type instance, the membership of any element $a \in \alpha$ in $s$ is decidable. This is established by checking whether $a$ belongs to the finite set representation of $s$ (via `s.toFinset`).
Set.coe_toFinset theorem
(s : Set α) [Fintype s] : (↑s.toFinset : Set α) = s
Full source 
@[simp]
theorem coe_toFinset (s : Set α) [Fintype s] : (↑s.toFinset : Set α) = s :=
  Set.ext fun _ => mem_toFinset
Equality of Set and its Finite Set Representation
Informal description
For any set $s$ over a finite type $\alpha$ with a `Fintype` instance, the underlying set of the finite set `s.toFinset` is equal to $s$ itself, i.e., $\uparrow(s.\mathrm{toFinset}) = s$.
Set.toFinset_nonempty theorem
{s : Set α} [Fintype s] : s.toFinset.Nonempty ↔ s.Nonempty
Full source 
@[simp]
theorem toFinset_nonempty {s : Set α} [Fintype s] : s.toFinset.Nonempty ↔ s.Nonempty := by
  rw [← Finset.coe_nonempty, coe_toFinset]
Nonempty Correspondence Between Set and Finset in Finite Types
Informal description
For any set $s$ over a finite type $\alpha$ with a `Fintype` instance, the finite set representation `s.toFinset` is nonempty if and only if the set $s$ itself is nonempty.
Set.toFinset_inj theorem
{s t : Set α} [Fintype s] [Fintype t] : s.toFinset = t.toFinset ↔ s = t
Full source 
@[simp]
theorem toFinset_inj {s t : Set α} [Fintype s] [Fintype t] : s.toFinset = t.toFinset ↔ s = t :=
  ⟨fun h => by rw [← s.coe_toFinset, h, t.coe_toFinset], fun h => by simp [h]⟩
Injectivity of Set-to-Finset Conversion in Finite Types
Informal description
For any two sets $s$ and $t$ over a finite type $\alpha$ with `Fintype` instances, the finite set representations of $s$ and $t$ (via `Set.toFinset`) are equal if and only if the sets themselves are equal, i.e., $s.\mathrm{toFinset} = t.\mathrm{toFinset} \leftrightarrow s = t$.
Set.toFinset_subset_toFinset theorem
[Fintype s] [Fintype t] : s.toFinset ⊆ t.toFinset ↔ s ⊆ t
Full source 
@[mono]
theorem toFinset_subset_toFinset [Fintype s] [Fintype t] : s.toFinset ⊆ t.toFinsets.toFinset ⊆ t.toFinset ↔ s ⊆ t := by
  simp [Finset.subset_iff, Set.subset_def]
Subset Correspondence Between Set and Finset Representations in Finite Types
Informal description
For any two sets $s$ and $t$ over a finite type $\alpha$ with `Fintype` instances, the finite set representation of $s$ is a subset of the finite set representation of $t$ if and only if $s$ is a subset of $t$. In other words, $s.\mathrm{toFinset} \subseteq t.\mathrm{toFinset} \leftrightarrow s \subseteq t$.
Set.toFinset_ssubset theorem
[Fintype s] {t : Finset α} : s.toFinset ⊂ t ↔ s ⊂ t
Full source 
@[simp]
theorem toFinset_ssubset [Fintype s] {t : Finset α} : s.toFinset ⊂ ts.toFinset ⊂ t ↔ s ⊂ t := by
  rw [← Finset.coe_ssubset, coe_toFinset]
Strict Subset Correspondence Between Set and Finset Representations in Finite Types
Informal description
For any set $s$ over a finite type $\alpha$ with a `Fintype` instance and any finite set $t$ of type $\alpha$, the finite set representation of $s$ (via `Set.toFinset`) is a strict subset of $t$ if and only if $s$ is a strict subset of the underlying set of $t$. In other words, $s.\mathrm{toFinset} \subset t \leftrightarrow s \subset t$.
Set.subset_toFinset theorem
{s : Finset α} [Fintype t] : s ⊆ t.toFinset ↔ ↑s ⊆ t
Full source 
@[simp]
theorem subset_toFinset {s : Finset α} [Fintype t] : s ⊆ t.toFinsets ⊆ t.toFinset ↔ ↑s ⊆ t := by
  rw [← Finset.coe_subset, coe_toFinset]
Subset Correspondence Between Finite Set and its Underlying Set Representation
Informal description
For any finite set $s$ of type $\alpha$ and any set $t$ over $\alpha$ with a `Fintype` instance, the finite set $s$ is a subset of the finite set representation of $t$ if and only if the underlying set of $s$ is a subset of $t$. In other words, $s \subseteq t.\mathrm{toFinset} \leftrightarrow \uparrow s \subseteq t$.
Set.ssubset_toFinset theorem
{s : Finset α} [Fintype t] : s ⊂ t.toFinset ↔ ↑s ⊂ t
Full source 
@[simp]
theorem ssubset_toFinset {s : Finset α} [Fintype t] : s ⊂ t.toFinsets ⊂ t.toFinset ↔ ↑s ⊂ t := by
  rw [← Finset.coe_ssubset, coe_toFinset]
Strict Subset Correspondence Between Finite Set and its Underlying Set Representation
Informal description
For any finite set $s$ of type $\alpha$ and any set $t$ over $\alpha$ with a `Fintype` instance, the finite set $s$ is a strict subset of the finite set representation of $t$ if and only if the underlying set of $s$ is a strict subset of $t$. In other words, $s \subset t.\mathrm{toFinset} \leftrightarrow \uparrow s \subset t$.
Set.toFinset_ssubset_toFinset theorem
[Fintype s] [Fintype t] : s.toFinset ⊂ t.toFinset ↔ s ⊂ t
Full source 
@[mono]
theorem toFinset_ssubset_toFinset [Fintype s] [Fintype t] : s.toFinset ⊂ t.toFinsets.toFinset ⊂ t.toFinset ↔ s ⊂ t := by
  simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]
Strict Subset Preservation under Finite Set Conversion
Informal description
For any sets $s$ and $t$ over a finite type $\alpha$ with `Fintype` instances, the finite set representation of $s$ is a strict subset of the finite set representation of $t$ if and only if $s$ is a strict subset of $t$. In other words, $s.\mathrm{toFinset} \subset t.\mathrm{toFinset} \leftrightarrow s \subset t$.
Set.toFinset_subset theorem
[Fintype s] {t : Finset α} : s.toFinset ⊆ t ↔ s ⊆ t
Full source 
@[simp]
theorem toFinset_subset [Fintype s] {t : Finset α} : s.toFinset ⊆ ts.toFinset ⊆ t ↔ s ⊆ t := by
  rw [← Finset.coe_subset, coe_toFinset]
Subset Correspondence Between Set and its Finite Representation
Informal description
For a set $s$ over a finite type $\alpha$ (with a `Fintype` instance for $s$) and a finite set $t$ over $\alpha$, the finite set representation of $s$ (via `s.toFinset`) is a subset of $t$ if and only if $s$ is a subset of the underlying set of $t$. In other words, $s.\mathrm{toFinset} \subseteq t \leftrightarrow s \subseteq t$.
Set.disjoint_toFinset theorem
[Fintype s] [Fintype t] : Disjoint s.toFinset t.toFinset ↔ Disjoint s t
Full source 
@[simp]
theorem disjoint_toFinset [Fintype s] [Fintype t] :
    DisjointDisjoint s.toFinset t.toFinset ↔ Disjoint s t := by simp only [← disjoint_coe, coe_toFinset]
Disjointness Preservation under Finite Set Conversion
Informal description
For any finite sets $s$ and $t$ over a finite type, the finite set representations $s.\mathrm{toFinset}$ and $t.\mathrm{toFinset}$ are disjoint if and only if the original sets $s$ and $t$ are disjoint, i.e., $s.\mathrm{toFinset} \cap t.\mathrm{toFinset} = \emptyset \leftrightarrow s \cap t = \emptyset$.
Set.toFinset_nontrivial theorem
[Fintype s] : s.toFinset.Nontrivial ↔ s.Nontrivial
Full source 
@[simp]
theorem toFinset_nontrivial [Fintype s] : s.toFinset.Nontrivial ↔ s.Nontrivial := by
  rw [Finset.Nontrivial, coe_toFinset]
Nontriviality Preservation in Finite Set Conversion
Informal description
For any set $s$ in a finite type $\alpha$ with a `Fintype` instance, the finite set representation $s.\mathrm{toFinset}$ is nontrivial (contains at least two distinct elements) if and only if the set $s$ itself is nontrivial.
Set.toFinset_inter theorem
[Fintype (s ∩ t : Set _)] : (s ∩ t).toFinset = s.toFinset ∩ t.toFinset
Full source 
@[simp]
theorem toFinset_inter [Fintype (s ∩ t : Set _)] : (s ∩ t).toFinset = s.toFinset ∩ t.toFinset := by
  ext
  simp
Finite Set Representation Preserves Intersection
Informal description
For any sets $s$ and $t$ over a finite type, if the intersection $s \cap t$ is finite, then the finite set representation of $s \cap t$ is equal to the intersection of the finite set representations of $s$ and $t$, i.e., $(s \cap t).\mathrm{toFinset} = s.\mathrm{toFinset} \cap t.\mathrm{toFinset}$.
Set.toFinset_union theorem
[Fintype (s ∪ t : Set _)] : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset
Full source 
@[simp]
theorem toFinset_union [Fintype (s ∪ t : Set _)] : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset := by
  ext
  simp
Union of Finite Sets Corresponds to Union of Their Finite Representations
Informal description
For any finite type $\alpha$ and sets $s, t \subseteq \alpha$ such that $s \cup t$ is finite, the finite set corresponding to the union $s \cup t$ is equal to the union of the finite sets corresponding to $s$ and $t$, i.e., $(s \cup t).\mathrm{toFinset} = s.\mathrm{toFinset} \cup t.\mathrm{toFinset}$.
Set.toFinset_diff theorem
[Fintype (s \ t : Set _)] : (s \ t).toFinset = s.toFinset \ t.toFinset
Full source 
@[simp]
theorem toFinset_diff [Fintype (s \ t : Set _)] : (s \ t).toFinset = s.toFinset \ t.toFinset := by
  ext
  simp
Finite Set Conversion Preserves Set Difference
Informal description
For any sets $s$ and $t$ over a finite type $\alpha$ such that the set difference $s \setminus t$ is finite, the finite set representation of $s \setminus t$ is equal to the set difference of the finite set representations of $s$ and $t$. That is, $(s \setminus t).\text{toFinset} = s.\text{toFinset} \setminus t.\text{toFinset}$.
Set.toFinset_symmDiff theorem
[Fintype (s ∆ t : Set _)] : (s ∆ t).toFinset = s.toFinset ∆ t.toFinset
Full source 
@[simp]
theorem toFinset_symmDiff [Fintype (s ∆ t : Set _)] :
    (s ∆ t).toFinset = s.toFinset ∆ t.toFinset := by
  ext
  simp [mem_symmDiff, Finset.mem_symmDiff]
Finite Set Conversion Preserves Symmetric Difference
Informal description
For any sets $s$ and $t$ over a finite type $\alpha$ such that the symmetric difference $s \triangle t$ is finite, the finite set representation of $s \triangle t$ is equal to the symmetric difference of the finite set representations of $s$ and $t$. That is, $(s \triangle t).\text{toFinset} = s.\text{toFinset} \triangle t.\text{toFinset}$.
Set.toFinset_compl theorem
[Fintype α] [Fintype (sᶜ : Set _)] : sᶜ.toFinset = s.toFinsetᶜ
Full source 
@[simp]
theorem toFinset_compl [Fintype α] [Fintype (sᶜ : Set _)] : sᶜ.toFinset = s.toFinsetᶜ := by
  ext
  simp
Complement of Finite Set Representation Equals Representation of Complement
Informal description
For a finite type $\alpha$ and a set $s \subseteq \alpha$ such that the complement $s^c$ is also finite, the finite set representation of $s^c$ is equal to the complement of the finite set representation of $s$. That is, $\mathrm{toFinset}(s^c) = (\mathrm{toFinset}\, s)^c$.
Set.toFinset_empty theorem
[Fintype (∅ : Set α)] : (∅ : Set α).toFinset = ∅
Full source 
@[simp]
theorem toFinset_empty [Fintype (∅ : Set α)] : (∅ : Set α).toFinset = ∅ := by
  ext
  simp
Empty Set to Finite Set Conversion Yields Empty Finite Set
Informal description
For any type $\alpha$, the conversion of the empty set $\emptyset$ to a finite set (via `toFinset`) results in the empty finite set $\emptyset$, provided that the empty set is finite (i.e., there exists a `Fintype` instance for $\emptyset$).
Set.toFinset_univ theorem
[Fintype α] [Fintype (Set.univ : Set α)] : (Set.univ : Set α).toFinset = Finset.univ
Full source 
@[simp]
theorem toFinset_univ [Fintype α] [Fintype (Set.univ : Set α)] :
    (Set.univ : Set α).toFinset = Finset.univ := by
  ext
  simp
Conversion of Universal Set to Universal Finite Set in Finite Types
Informal description
For a finite type $\alpha$ where the universal set $\mathrm{univ} : \mathrm{Set}\,\alpha$ is finite, the conversion of $\mathrm{univ}$ to a finite set via $\mathrm{toFinset}$ yields the universal finite set $\mathrm{Finset.univ}$ of $\alpha$. That is, $\mathrm{toFinset}(\mathrm{univ}) = \mathrm{Finset.univ}$.
Set.toFinset_eq_empty theorem
[Fintype s] : s.toFinset = ∅ ↔ s = ∅
Full source 
@[simp]
theorem toFinset_eq_empty [Fintype s] : s.toFinset = ∅ ↔ s = ∅ := by
  let A : Fintype (∅ : Set α) := Fintype.ofIsEmpty
  rw [← toFinset_empty, toFinset_inj]
Empty Set Equivalence in Finite Types
Informal description
For a finite set $s$ (with a `Fintype` instance), the finite set representation of $s$ (via `toFinset`) is empty if and only if $s$ is the empty set. In other words: $$s.\mathrm{toFinset} = \emptyset \leftrightarrow s = \emptyset.$$
Set.toFinset_eq_univ theorem
[Fintype α] [Fintype s] : s.toFinset = Finset.univ ↔ s = univ
Full source 
@[simp]
theorem toFinset_eq_univ [Fintype α] [Fintype s] : s.toFinset = Finset.univ ↔ s = univ := by
  rw [← coe_inj, coe_toFinset, coe_univ]
Equivalence of Universal Set and its Finite Representation in Finite Types
Informal description
For a finite type $\alpha$ and a subset $s$ of $\alpha$ that is also finite, the finite set representation of $s$ (via `toFinset`) equals the universal finite set of $\alpha$ if and only if $s$ is the universal set of $\alpha$. In other words: $$s.\mathrm{toFinset} = \mathrm{Finset.univ} \leftrightarrow s = \mathrm{Set.univ}.$$
Set.toFinset_setOf theorem
[Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {x | p x}] : Set.toFinset {x | p x} = Finset.univ.filter p
Full source 
@[simp]
theorem toFinset_setOf [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { x | p x }] :
    Set.toFinset {x | p x} = Finset.univ.filter p := by
  ext
  simp
Conversion of Set Comprehension to Filtered Finset in Finite Types
Informal description
Let $\alpha$ be a finite type with a decidable predicate $p : \alpha \to \mathrm{Prop}$. Then the finite set corresponding to the subset $\{x \mid p x\}$ is equal to the filter of the universal finite set of $\alpha$ with respect to $p$, i.e., $$\mathrm{toFinset}\, \{x \mid p x\} = \mathrm{univ}.\mathrm{filter}\, p.$$
Set.toFinset_ssubset_univ theorem
[Fintype α] {s : Set α} [Fintype s] : s.toFinset ⊂ Finset.univ ↔ s ⊂ univ
Full source 
theorem toFinset_ssubset_univ [Fintype α] {s : Set α} [Fintype s] :
    s.toFinset ⊂ Finset.univs.toFinset ⊂ Finset.univ ↔ s ⊂ univ := by simp
Strict Subset Correspondence Between Finite Set Representation and Universal Set in Finite Types
Informal description
For a finite type $\alpha$ and a subset $s \subseteq \alpha$ that is also finite, the finite set representation of $s$ is a strict subset of the universal finite set of $\alpha$ if and only if $s$ is a strict subset of the universal set of $\alpha$. In other words: $$s.\mathrm{toFinset} \subset \mathrm{Finset.univ} \leftrightarrow s \subset \mathrm{Set.univ}.$$
Set.toFinset_image theorem
[DecidableEq β] (f : α → β) (s : Set α) [Fintype s] [Fintype (f '' s)] : (f '' s).toFinset = s.toFinset.image f
Full source 
@[simp]
theorem toFinset_image [DecidableEq β] (f : α → β) (s : Set α) [Fintype s] [Fintype (f '' s)] :
    (f '' s).toFinset = s.toFinset.image f :=
  Finset.coe_injective <| by simp
Image of Finite Set under Function Preserves Finset Conversion
Informal description
Let $\alpha$ and $\beta$ be types with decidable equality on $\beta$, and let $f : \alpha \to \beta$ be a function. For any finite subset $s \subseteq \alpha$ such that the image $f(s) \subseteq \beta$ is also finite, the finite set obtained by converting $f(s)$ to a `Finset` is equal to the image of the finite set representation of $s$ under $f$, i.e., $$(f(s)).\mathrm{toFinset} = s.\mathrm{toFinset}.\mathrm{image}\, f.$$
Set.toFinset_range theorem
[DecidableEq α] [Fintype β] (f : β → α) [Fintype (Set.range f)] : (Set.range f).toFinset = Finset.univ.image f
Full source 
@[simp]
theorem toFinset_range [DecidableEq α] [Fintype β] (f : β → α) [Fintype (Set.range f)] :
    (Set.range f).toFinset = Finset.univ.image f := by
  ext
  simp
Range of a Function on Finite Types as Image of Universal Set
Informal description
Let $\alpha$ and $\beta$ be finite types with decidable equality on $\alpha$, and let $f : \beta \to \alpha$ be a function. Then the finite set corresponding to the range of $f$ is equal to the image of the universal finite set of $\beta$ under $f$, i.e., $$\mathrm{toFinset}(\mathrm{range}\, f) = \mathrm{image}\, f\, \mathrm{univ}.$$
Set.toFinset_singleton theorem
(a : α) [Fintype ({ a } : Set α)] : ({ a } : Set α).toFinset = { a }
Full source 
@[simp]
theorem toFinset_singleton (a : α) [Fintype ({a} : Set α)] : ({a} : Set α).toFinset = {a} := by
  ext
  simp
Conversion of Singleton Set to Finite Set
Informal description
For any element $a$ of a type $\alpha$ where the singleton set $\{a\}$ is finite, the finite set obtained by converting $\{a\}$ to a `Finset` is equal to the singleton finite set $\{a\}$.
Set.toFinset_insert theorem
[DecidableEq α] {a : α} {s : Set α} [Fintype (insert a s : Set α)] [Fintype s] : (insert a s).toFinset = insert a s.toFinset
Full source 
@[simp]
theorem toFinset_insert [DecidableEq α] {a : α} {s : Set α} [Fintype (insert a s : Set α)]
    [Fintype s] : (insert a s).toFinset = insert a s.toFinset := by
  ext
  simp
Insertion Commutes with Conversion to Finite Set
Informal description
Let $\alpha$ be a type with decidable equality, and let $a \in \alpha$ and $s \subseteq \alpha$ be a set. If both the set $\{a\} \cup s$ and $s$ are finite, then the finite set corresponding to $\{a\} \cup s$ is equal to the insertion of $a$ into the finite set corresponding to $s$, i.e., $$(\{a\} \cup s).\mathrm{toFinset} = \{a\} \cup s.\mathrm{toFinset}.$$
Set.filter_mem_univ_eq_toFinset theorem
[Fintype α] (s : Set α) [Fintype s] [DecidablePred (· ∈ s)] : Finset.univ.filter (· ∈ s) = s.toFinset
Full source 
theorem filter_mem_univ_eq_toFinset [Fintype α] (s : Set α) [Fintype s] [DecidablePred (· ∈ s)] :
    Finset.univ.filter (· ∈ s) = s.toFinset := by
  ext
  simp only [Finset.mem_univ, decide_eq_true_eq, forall_true_left, mem_filter,
    true_and, mem_toFinset]
Equality of Filtered Universal Set and Subset's Finite Set Representation
Informal description
Let $\alpha$ be a finite type, and let $s$ be a subset of $\alpha$ that is also finite. If membership in $s$ is decidable, then the finite set obtained by filtering the universal finite set of $\alpha$ to retain only elements of $s$ is equal to the finite set representation of $s$.
Finset.toFinset_coe theorem
(s : Finset α) [Fintype (s : Set α)] : (s : Set α).toFinset = s
Full source 
@[simp]
theorem Finset.toFinset_coe (s : Finset α) [Fintype (s : Set α)] : (s : Set α).toFinset = s :=
  ext fun _ => Set.mem_toFinset
Conversion from Finset to Set and Back Preserves Identity
Informal description
For any finite set $s$ of type $\alpha$ (viewed as a subset of $\alpha$), if the subset $s$ has a `Fintype` instance, then the conversion of $s$ to a finite set via `Set.toFinset` yields $s$ itself. In other words, $(s : \mathrm{Set} \alpha).\mathrm{toFinset} = s$.
Finset.fintypeCoeSort instance
{α : Type u} (s : Finset α) : Fintype s
Full source 
instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) : Fintype s :=
  ⟨s.attach, s.mem_attach⟩
Finsets are Finite Types
Informal description
For any finset $s$ of a type $\alpha$, the subtype corresponding to $s$ is a finite type.
Finset.univ_eq_attach theorem
{α : Type u} (s : Finset α) : (univ : Finset s) = s.attach
Full source 
@[simp]
theorem Finset.univ_eq_attach {α : Type u} (s : Finset α) : (univ : Finset s) = s.attach :=
  rfl
Universal Finset of Subtype Equals Attached Finset
Informal description
For any finset $s$ of a type $\alpha$, the universal finset of the subtype corresponding to $s$ is equal to the attached finset of $s$.
Fintype.coe_image_univ theorem
[Fintype α] [DecidableEq β] {f : α → β} : ↑(Finset.image f Finset.univ) = Set.range f
Full source 
theorem Fintype.coe_image_univ [Fintype α] [DecidableEq β] {f : α → β} :
    ↑(Finset.image f Finset.univ) = Set.range f := by
  ext x
  simp
Image of Universal Finset Equals Range of Function
Informal description
For a finite type $\alpha$ and a function $f : \alpha \to \beta$ (with decidable equality on $\beta$), the image of the universal finset under $f$ is equal to the range of $f$ as sets. In other words, $f(\text{univ}) = \text{range}(f)$ where $\text{univ}$ is the universal finset containing all elements of $\alpha$.
FinsetCoe.fintype instance
(s : Finset α) : Fintype (↑s : Set α)
Full source 
instance FinsetCoe.fintype (s : Finset α) : Fintype (↑s : Set α) :=
  Finset.Subtype.fintype s
Finiteness of Sets Corresponding to Finsets
Informal description
For any finset $s$ of elements of type $\alpha$, the set $\{x \mid x \in s\}$ is a finite type.
Finset.attach_eq_univ theorem
{s : Finset α} : s.attach = Finset.univ
Full source 
theorem Finset.attach_eq_univ {s : Finset α} : s.attach = Finset.univ :=
  rfl
Attached Subtype Equals Universal Finite Set
Informal description
For any finite set $s$ of elements of type $\alpha$, the attached set (the subtype $\{x \mid x \in s\}$) is equal to the universal finite set of its type.
Fintype.univ_Prop theorem
: (Finset.univ : Finset Prop) = { True, False }
Full source 
@[simp]
theorem Fintype.univ_Prop : (Finset.univ : Finset Prop) = {True, False} :=
  Finset.eq_of_veq <| by simp; rfl
Universal Finite Set of Propositions Equals $\{\text{True}, \text{False}\}$
Informal description
The universal finite set of propositions consists exactly of the two elements `True` and `False`, i.e., $\text{Finset.univ} = \{\text{True}, \text{False}\}$.
Subtype.fintype instance
(p : α → Prop) [DecidablePred p] [Fintype α] : Fintype { x // p x }
Full source 
instance Subtype.fintype (p : α → Prop) [DecidablePred p] [Fintype α] : Fintype { x // p x } :=
  Fintype.subtype (univ.filter p) (by simp)
Finite Subtype of a Finite Type
Informal description
For any type $\alpha$ with a finite type structure and a decidable predicate $p : \alpha \to \mathrm{Prop}$, the subtype $\{x \mid p(x)\}$ is also a finite type.
setFintype definition
[Fintype α] (s : Set α) [DecidablePred (· ∈ s)] : Fintype s
Full source 
/-- A set on a fintype, when coerced to a type, is a fintype. -/
def setFintype [Fintype α] (s : Set α) [DecidablePred (· ∈ s)] : Fintype s :=
  Subtype.fintype fun x => x ∈ s
Finite type structure on a decidable subset of a finite type
Informal description
Given a finite type $\alpha$ and a decidable subset $s$ of $\alpha$, the type of elements of $s$ is also finite. This is constructed by viewing $s$ as a subtype of $\alpha$ and using the fact that any decidable subtype of a finite type is finite.
Fintype.finsetEquivSet definition
: Finset α ≃ Set α
Full source 
/-- Given `Fintype α`, `finsetEquivSet` is the equiv between `Finset α` and `Set α`. (All
sets on a finite type are finite.) -/
noncomputable def finsetEquivSet : FinsetFinset α ≃ Set α where
  toFun := (↑)
  invFun := by classical exact fun s => s.toFinset
  left_inv s := by convert Finset.toFinset_coe s
  right_inv s := by classical exact s.coe_toFinset
Equivalence between finite sets and subsets of a finite type
Informal description
Given a finite type $\alpha$, the function `Fintype.finsetEquivSet` is an equivalence (bijection) between the type of finite sets `Finset α` and the type of all subsets `Set α`. This equivalence is constructed by: 1. The forward map is the canonical inclusion from `Finset α` to `Set α`. 2. The inverse map converts a set $s$ to a finite set using `Set.toFinset`, which is well-defined since all subsets of a finite type are finite. 3. The left inverse property states that converting a finite set to a set and back yields the original finite set. 4. The right inverse property states that converting a set to a finite set and back yields the original set.
Fintype.coe_finsetEquivSet theorem
: ⇑finsetEquivSet = ((↑) : Finset α → Set α)
Full source 
@[simp, norm_cast] lemma coe_finsetEquivSet : ⇑finsetEquivSet = ((↑) : Finset α → Set α) := rfl
Equivalence between finite sets and subsets coincides with canonical inclusion
Informal description
The equivalence `finsetEquivSet` between finite sets and subsets of a finite type $\alpha$ is equal to the canonical inclusion map from `Finset α` to `Set α`. In other words, the forward map of the equivalence is simply the coercion from finite sets to sets.
Fintype.finsetEquivSet_apply theorem
(s : Finset α) : finsetEquivSet s = s
Full source 
@[simp] lemma finsetEquivSet_apply (s : Finset α) : finsetEquivSet s = s := rfl
Identity Mapping of Finite Sets under `finsetEquivSet`
Informal description
For any finite set $s$ of elements in a finite type $\alpha$, the equivalence `finsetEquivSet` maps $s$ to itself when viewed as a subset of $\alpha$. In other words, the canonical inclusion from finite sets to subsets is the identity on finite sets.
Fintype.finsetEquivSet_symm_apply theorem
(s : Set α) [Fintype s] : finsetEquivSet.symm s = s.toFinset
Full source 
@[simp] lemma finsetEquivSet_symm_apply (s : Set α) [Fintype s] :
    finsetEquivSet.symm s = s.toFinset := by simp [finsetEquivSet]
Inverse of Finset-Set Equivalence Maps Subset to Finite Set
Informal description
For any subset $s$ of a finite type $\alpha$ (with a `Fintype` instance for $s$), the inverse of the equivalence between finite sets and subsets of $\alpha$ maps $s$ to its corresponding finite set, i.e., $\text{finsetEquivSet}^{-1}(s) = \text{toFinset}(s)$.
Fintype.finsetOrderIsoSet definition
: Finset α ≃o Set α
Full source 
/-- Given a fintype `α`, `finsetOrderIsoSet` is the order isomorphism between `Finset α` and `Set α`
(all sets on a finite type are finite). -/
@[simps toEquiv]
noncomputable def finsetOrderIsoSet : FinsetFinset α ≃o Set α where
  toEquiv := finsetEquivSet
  map_rel_iff' := Finset.coe_subset
Order isomorphism between finite sets and subsets of a finite type
Informal description
Given a finite type $\alpha$, the function `Fintype.finsetOrderIsoSet` is an order isomorphism between the type of finite sets `Finset α` and the type of all subsets `Set α`. This means: 1. It is a bijection that preserves the order structure, where the order on `Finset α` and `Set α` is given by subset inclusion. 2. The forward map is the canonical inclusion from `Finset α` to `Set α`. 3. The inverse map converts a set $s$ to a finite set using `Set.toFinset`, which is well-defined since all subsets of a finite type are finite. 4. The order-preserving property states that for any two finite sets $s_1, s_2 \in \text{Finset } \alpha$, we have $s_1 \subseteq s_2$ if and only if their images under the isomorphism are subsets in $\text{Set } \alpha$.
Fintype.coe_finsetOrderIsoSet theorem
: ⇑finsetOrderIsoSet = ((↑) : Finset α → Set α)
Full source 
@[simp, norm_cast]
lemma coe_finsetOrderIsoSet : ⇑finsetOrderIsoSet = ((↑) : Finset α → Set α) := rfl
Canonical Inclusion as Order Isomorphism Function
Informal description
The underlying function of the order isomorphism `finsetOrderIsoSet` between `Finset α` and `Set α` is equal to the canonical inclusion map from `Finset α` to `Set α`.
Fintype.coe_finsetOrderIsoSet_symm theorem
: ⇑(finsetOrderIsoSet : Finset α ≃o Set α).symm = ⇑finsetEquivSet.symm
Full source 
@[simp] lemma coe_finsetOrderIsoSet_symm :
    ⇑(finsetOrderIsoSet : FinsetFinset α ≃o Set α).symm = ⇑finsetEquivSet.symm := rfl
Inverse of Order Isomorphism Equals Inverse of Set Equivalence for Finite Types
Informal description
The inverse of the order isomorphism `finsetOrderIsoSet` between finite sets and subsets of a finite type $\alpha$ is equal to the inverse of the equivalence `finsetEquivSet` between these types. In other words, the inverse map of the order isomorphism coincides with the inverse map of the underlying set equivalence.
mem_image_univ_iff_mem_range theorem
{α β : Type*} [Fintype α] [DecidableEq β] {f : α → β} {b : β} : b ∈ univ.image f ↔ b ∈ Set.range f
Full source 
theorem mem_image_univ_iff_mem_range {α β : Type*} [Fintype α] [DecidableEq β] {f : α → β}
    {b : β} : b ∈ univ.image fb ∈ univ.image f ↔ b ∈ Set.range f := by simp
Image of Universal Finset Equals Range of Function
Informal description
For a finite type $\alpha$ and a function $f : \alpha \to \beta$ with $\beta$ having decidable equality, an element $b \in \beta$ belongs to the image of $f$ over the universal finset of $\alpha$ if and only if $b$ is in the range of $f$. In other words, $b \in \text{image } f \text{ univ} \leftrightarrow b \in \text{range } f$.
finsetStx definition
: Lean.ParserDescr✝
Full source 
/-- `finset% t` elaborates `t` as a `Finset`.
If `t` is a `Set`, then inserts `Set.toFinset`.
Does not make use of the expected type; useful for big operators over finsets.
```
#check finset% Finset.range 2 -- Finset Nat
#check finset% (Set.univ : Set Bool) -- Finset Bool
```
-/
elab (name := finsetStx) "finset% " t:term : term => do
  let u ← mkFreshLevelMVar
  let ty ← mkFreshExprMVar (mkSort (.succ u))
  let x ← Elab.Term.elabTerm t (mkApp (.const ``Finset [u]) ty)
  let xty ← whnfR (← inferType x)
  if xty.isAppOfArity ``Set 1 then
    Elab.Term.elabAppArgs (.const ``Set.toFinset [u]) #[] #[.expr x] none false false
  else
    return x
Finset elaboration macro
Informal description
The `finset%` macro elaborates a term `t` as a `Finset`. If `t` is a `Set`, it automatically inserts `Set.toFinset` to convert the set to a finset. This macro does not rely on the expected type and is particularly useful for big operators over finsets.
precheckFinsetStx definition
: Precheck
Full source 
/-- `quot_precheck` for the `finset%` syntax. -/
@[quot_precheck finsetStx] def precheckFinsetStx : Precheck
  | `(finset% $t) => precheck t
  | _ => Elab.throwUnsupportedSyntax
Precheck for `finset%` syntax
Informal description
The `precheckFinsetStx` definition is a parser precheck for the `finset%` syntax, which ensures that the input term `t` is valid before further processing. Specifically, it checks the syntax of the term `t` when used in a `finset%` context and throws an error if the syntax is unsupported.