# Subsets of finite types #

In a `Fintype`, all `Set`s are automatically `Finset`s, 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`

source
def Set.toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :
Finset α

Construct a finset enumerating a set `s`, given a `Fintype` instance.

Equations

- s.toFinset = Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ s) Finset.univ

Instances For

source
theorem Set.toFinset_congr {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] (h : s = t) :
s.toFinset = t.toFinset
source
@[simp]
theorem Set.mem_toFinset {α : Type u_1} {s : Set α} [Fintype ↑s] {a : α} :
a ∈ s.toFinset ↔ a ∈ s
source
theorem Set.toFinset_ofFinset {α : Type u_1} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) :
p.toFinset = s

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`.

source
def Set.decidableMemOfFintype {α : Type u_1} [DecidableEq α] (s : Set α) [Fintype ↑s] (a : α) :
Decidable (a ∈ s)

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.

Equations

- s.decidableMemOfFintype a = decidable_of_iff (a ∈ s.toFinset) ⋯

Instances For

source
@[simp]
theorem Set.coe_toFinset {α : Type u_1} (s : Set α) [Fintype ↑s] :
↑s.toFinset = s
source
@[simp]
theorem Set.toFinset_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] :
s.toFinset.Nonempty ↔ s.Nonempty
source
theorem Set.Aesop.toFinset_nonempty_of_nonempty {α : Type u_1} {s : Set α} [Fintype ↑s] :
s.Nonempty → s.toFinset.Nonempty

Alias of the reverse direction of `Set.toFinset_nonempty`.

source
@[simp]
theorem Set.toFinset_inj {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
s.toFinset = t.toFinset ↔ s = t
source
theorem Set.toFinset_subset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
s.toFinset ⊆ t.toFinset ↔ s ⊆ t
source
@[simp]
theorem Set.toFinset_ssubset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :
s.toFinset ⊂ t ↔ s ⊂ ↑t
source
@[simp]
theorem Set.subset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :
s ⊆ t.toFinset ↔ ↑s ⊆ t
source
@[simp]
theorem Set.ssubset_toFinset {α : Type u_1} {t : Set α} {s : Finset α} [Fintype ↑t] :
s ⊂ t.toFinset ↔ ↑s ⊂ t
source
theorem Set.toFinset_ssubset_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
s.toFinset ⊂ t.toFinset ↔ s ⊂ t
source
@[simp]
theorem Set.toFinset_subset {α : Type u_1} {s : Set α} [Fintype ↑s] {t : Finset α} :
s.toFinset ⊆ t ↔ s ⊆ ↑t
source
theorem Set.toFinset_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
s ⊆ t → s.toFinset ⊆ t.toFinset

Alias of the reverse direction of `Set.toFinset_subset_toFinset`.

source
@[deprecated Set.toFinset_mono (since := "2025-10-25")]
theorem Set.toFinset_subset_toFinset_of_subset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
s ⊆ t → s.toFinset ⊆ t.toFinset

Alias of the reverse direction of `Set.toFinset_subset_toFinset`.

Alias of the reverse direction of `Set.toFinset_subset_toFinset`.

source
theorem Set.toFinset_strict_mono {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
s ⊂ t → s.toFinset ⊂ t.toFinset

Alias of the reverse direction of `Set.toFinset_ssubset_toFinset`.

source
@[simp]
theorem Set.disjoint_toFinset {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] :
Disjoint s.toFinset t.toFinset ↔ Disjoint s t
source
@[simp]
theorem Set.toFinset_nontrivial {α : Type u_1} {s : Set α} [Fintype ↑s] :
s.toFinset.Nontrivial ↔ s.Nontrivial
source
@[simp]
theorem Set.toFinset_inter {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∩ t)] :
(s ∩ t).toFinset = s.toFinset ∩ t.toFinset
source
@[simp]
theorem Set.toFinset_union {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s ∪ t)] :
(s ∪ t).toFinset = s.toFinset ∪ t.toFinset
source
@[simp]
theorem Set.toFinset_diff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(s \ t)] :
(s \ t).toFinset = s.toFinset \ t.toFinset
source
@[simp]
theorem Set.toFinset_symmDiff {α : Type u_1} (s t : Set α) [DecidableEq α] [Fintype ↑s] [Fintype ↑t] [Fintype ↑(symmDiff s t)] :
(symmDiff s t).toFinset = symmDiff s.toFinset t.toFinset
source
@[simp]
theorem Set.toFinset_compl {α : Type u_1} (s : Set α) [DecidableEq α] [Fintype ↑s] [Fintype α] [Fintype ↑s ᶜ] :
s ᶜ.toFinset = s.toFinset ᶜ
source
@[simp]
theorem Set.toFinset_empty {α : Type u_1} [Fintype ↑∅] :
∅.toFinset = ∅
source
@[simp]
theorem Set.toFinset_univ {α : Type u_1} [Fintype α] [Fintype ↑univ] :
univ.toFinset = Finset.univ
source
@[simp]
theorem Set.toFinset_eq_empty {α : Type u_1} {s : Set α} [Fintype ↑s] :
s.toFinset = ∅ ↔ s = ∅
source
@[simp]
theorem Set.toFinset_eq_univ {α : Type u_1} {s : Set α} [Fintype α] [Fintype ↑s] :
s.toFinset = Finset.univ ↔ s = univ
source
@[simp]
theorem Set.toFinset_setOf {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype ↑{x : α | p x}] :
{x : α | p x}.toFinset = Finset.filter p Finset.univ
source
theorem Set.toFinset_ssubset_univ {α : Type u_1} [Fintype α] {s : Set α} [Fintype ↑s] :
s.toFinset ⊂ Finset.univ ↔ s ⊂ univ
source
@[simp]
theorem Set.toFinset_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Set α) [Fintype ↑s] [Fintype ↑(f '' s)] :
(f '' s).toFinset = Finset.image f s.toFinset
source
@[simp]
theorem Set.toFinset_range {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] (f : β → α) [Fintype ↑(range f)] :
(range f).toFinset = Finset.image f Finset.univ
source
@[simp]
theorem Set.toFinset_singleton {α : Type u_1} (a : α) [Fintype ↑{a}] :
{a}.toFinset = {a}
source
@[simp]
theorem Set.toFinset_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Set α} [Fintype ↑(insert a s)] [Fintype ↑s] :
(insert a s).toFinset = insert a s.toFinset
source
theorem Set.filter_mem_univ_eq_toFinset {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ s] :
{x : α | x ∈ s} = s.toFinset
source
@[simp]
theorem Finset.toFinset_coe {α : Type u_1} (s : Finset α) [Fintype ↑↑s] :
(↑s).toFinset = s

### `Fintype (s : Finset α)` #

source
instance Finset.fintypeCoeSort {α : Type u} (s : Finset α) :
Fintype ↥s
Equations

- s.fintypeCoeSort = { elems := s.attach, complete := ⋯ }

source
@[simp]
theorem Finset.univ_eq_attach {α : Type u} (s : Finset α) :
univ = s.attach
source
theorem Fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} :
↑(Finset.image f Finset.univ) = Set.range f
source
instance List.Subtype.fintype {α : Type u_1} [DecidableEq α] (l : List α) :
Fintype { x : α // x ∈ l }
Equations

- List.Subtype.fintype l = Fintype.ofList l.attach ⋯

source
instance Multiset.Subtype.fintype {α : Type u_1} [DecidableEq α] (s : Multiset α) :
Fintype { x : α // x ∈ s }
Equations

- Multiset.Subtype.fintype s = Fintype.ofMultiset s.attach ⋯

source
instance Finset.Subtype.fintype {α : Type u_1} (s : Finset α) :
Fintype { x : α // x ∈ s }
Equations

- Finset.Subtype.fintype s = { elems := s.attach, complete := ⋯ }

source
instance FinsetCoe.fintype {α : Type u_1} (s : Finset α) :
Fintype ↑↑s
Equations

- FinsetCoe.fintype s = Finset.Subtype.fintype s

source
theorem Finset.attach_eq_univ {α : Type u_1} {s : Finset α} :
s.attach = univ
source
instance Prop.fintype :
Fintype Prop
Equations

- «Prop».fintype = { elems := { val := {True, False}, nodup := «Prop».fintype._proof_1 }, complete := «Prop».fintype._proof_2 }

source
@[simp]
theorem Fintype.univ_Prop :
Finset.univ = {True, False}
source
instance Subtype.fintype {α : Type u_1} (p : α → Prop) [DecidablePred p] [Fintype α] :
Fintype { x : α // p x }
Equations

- Subtype.fintype p = Fintype.subtype (Finset.filter p Finset.univ) ⋯

source
def setFintype {α : Type u_1} [Fintype α] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] :
Fintype ↑s

A set on a fintype, when coerced to a type, is a fintype.

Equations

- setFintype s = Subtype.fintype fun (x : α) => x ∈ s

Instances For

source
noncomputable def Fintype.finsetEquivSet {α : Type u_1} [Fintype α] :
Finset α ≃ Set α

Given `Fintype α`, `finsetEquivSet` is the equiv between `Finset α` and `Set α`. (All sets on a finite type are finite.)

Equations

- Fintype.finsetEquivSet = { toFun := SetLike.coe, invFun := fun (s : Set α) => s.toFinset, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Fintype.coe_finsetEquivSet {α : Type u_1} [Fintype α] :
⇑finsetEquivSet = SetLike.coe
source
@[simp]
theorem Fintype.finsetEquivSet_apply {α : Type u_1} [Fintype α] (s : Finset α) :
finsetEquivSet s = ↑s
source
@[simp]
theorem Fintype.finsetEquivSet_symm_apply {α : Type u_1} [Fintype α] (s : Set α) [Fintype ↑s] :
finsetEquivSet.symm s = s.toFinset
source
noncomputable def Fintype.finsetOrderIsoSet {α : Type u_1} [Fintype α] :
Finset α ≃o Set α

Given a fintype `α`, `finsetOrderIsoSet` is the order isomorphism between `Finset α` and `Set α` (all sets on a finite type are finite).

Equations

- Fintype.finsetOrderIsoSet = { toEquiv := Fintype.finsetEquivSet, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem Fintype.finsetOrderIsoSet_toEquiv {α : Type u_1} [Fintype α] :
finsetOrderIsoSet.toEquiv = finsetEquivSet
source
@[simp]
theorem Fintype.coe_finsetOrderIsoSet {α : Type u_1} [Fintype α] :
⇑finsetOrderIsoSet = SetLike.coe
source
@[simp]
theorem Fintype.coe_finsetOrderIsoSet_symm {α : Type u_1} [Fintype α] :
⇑finsetOrderIsoSet.symm = ⇑finsetEquivSet.symm
source
theorem mem_image_univ_iff_mem_range {α : Type u_4} {β : Type u_5} [Fintype α] [DecidableEq β] {f : α → β} {b : β} :
b ∈ Finset.image f Finset.univ ↔ b ∈ Set.range f
source
def finsetStx :
Lean.ParserDescr

`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

Equations

- finsetStx = Lean.ParserDescr.node `finsetStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "finset% ") (Lean.ParserDescr.cat `term 0))

Instances For

source
def precheckFinsetStx :
Lean.Elab.Term.Quotation.Precheck

`quot_precheck` for the `finset%` syntax.

Equations

- One or more equations did not get rendered due to their size.

Instances For