Finite sets

Terms of type Finset α are one way of talking about finite subsets of α in Mathlib. Below, Finset α is defined as a structure with 2 fields:

1. val is a Multiset α of elements;
2. nodup is a proof that val has no duplicates.

Finsets in Lean are constructive in that they have an underlying List that enumerates their elements. In particular, any function that uses the data of the underlying list cannot depend on its ordering. This is handled on the Multiset level by multiset API, so in most cases one needn't worry about it explicitly.

Finsets give a basic foundation for defining finite sums and products over types:

1. ∑ i ∈ (s : Finset α), f i;
2. ∏ i ∈ (s : Finset α), f i.

Lean refers to these operations as big operators. More information can be found in Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean.

Finsets are directly used to define fintypes in Lean. A Fintype α instance for a type α consists of a universal Finset α containing every term of α, called univ. See Mathlib/Data/Fintype/Basic.lean.

Finset.card, the size of a finset is defined in Mathlib/Data/Finset/Card.lean. This is then used to define Fintype.card, the size of a type.

File structure

This file defines the Finset type and the membership and subset relations between finsets. Most constructions involving Finsets have been split off to their own files.

Main definitions

• Finset: Defines a type for the finite subsets of α. Constructing a Finset requires two pieces of data: val, a Multiset α of elements, and nodup, a proof that val has no duplicates.
• a ∈ (s : Finset α) is defined through coercion to Set α.

Tags

finite sets, finset

structure Finset (α : Type u_4) : Type u_4

Finset α is the type of finite sets of elements of α. It is implemented as a multiset (a list up to permutation) which has no duplicate elements.

• val : Multiset α

  The underlying multiset

• nodup : self.val.Nodup

  val contains no duplicates

instance Multiset.canLiftFinset {α : Type u_4} : CanLift (Multiset α) (Finset α) Finset.val Nodup

theorem Finset.eq_of_veq {α : Type u_1} {s t : Finset α} : s.val = t.val → s = t

theorem Finset.val_injective {α : Type u_1} : Function.Injective val

@[simp]

theorem Finset.val_inj {α : Type u_1} {s t : Finset α} : s.val = t.val ↔ s = t

@[implicit_reducible]

instance Finset.decidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Finset α)

Equations

• x✝¹.decidableEq x✝ = decidable_of_iff (x✝¹.val = x✝.val) ⋯

set coercion

@[implicit_reducible]

instance Finset.instSetLike {α : Type u_1} : SetLike (Finset α) α

Convert a finset to a set in the natural way.

Equations

• Finset.instSetLike = { coe := fun (s : Finset α) => {a : α | a ∈ s.val}, coe_injective := ⋯ }

theorem Finset.mem_def {α : Type u_1} {a : α} {s : Finset α} : a ∈ s ↔ a ∈ s.val

@[simp]

theorem Finset.mem_val {α : Type u_1} {a : α} {s : Finset α} : (a ∈ s.val) = (a ∈ s)

@[simp]

theorem Finset.mem_mk {α : Type u_1} {a : α} {s : Multiset α} {nd : s.Nodup} : a ∈ { val := s, nodup := nd } ↔ a ∈ s

@[implicit_reducible]

instance Finset.decidableMem {α : Type u_1} [_h : DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ s)

Equations

• Finset.decidableMem a s = Multiset.decidableMem a s.val

@[simp]

theorem Finset.forall_mem_not_eq {α : Type u_1} {s : Finset α} {a : α} : (∀ (b : α), b ∈ s → ¬a = b) ↔ ¬a ∈ s

@[simp]

theorem Finset.forall_mem_not_eq' {α : Type u_1} {s : Finset α} {a : α} : (∀ (b : α), b ∈ s → ¬b = a) ↔ ¬a ∈ s

@[implicit_reducible]

instance Finset.instPartialOrder {α : Type u_1} : PartialOrder (Finset α)

Equations

• Finset.instPartialOrder = PartialOrder.ofSetLike (Finset α) α

theorem Finset.mem_coe {α : Type u_1} {a : α} {s : Finset α} : a ∈ ↑s ↔ a ∈ s

@[simp]

theorem Finset.setOf_mem {α : Type u_4} {s : Finset α} : {a : α | a ∈ s} = ↑s

theorem Finset.coe_mem {α : Type u_1} {s : Finset α} (x : ↑↑s) : ↑x ∈ s

theorem Finset.mk_coe {α : Type u_1} {s : Finset α} (x : ↑↑s) {h : ↑x ∈ ↑s} : ⟨↑x, h⟩ = x

@[implicit_reducible]

instance Finset.decidableMem' {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : Decidable (a ∈ ↑s)

Equations

• Finset.decidableMem' a s = Finset.decidableMem a s

extensionality

theorem Finset.ext {α : Type u_1} {s₁ s₂ : Finset α} (h : ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂) : s₁ = s₂

theorem Finset.ext_iff {α : Type u_1} {s₁ s₂ : Finset α} : s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂

theorem Finset.coe_inj {α : Type u_1} {s₁ s₂ : Finset α} : ↑s₁ = ↑s₂ ↔ s₁ = s₂

theorem Finset.coe_injective {α : Type u_4} : Function.Injective SetLike.coe

type coercion

theorem Finset.forall_coe {α : Type u_4} (s : Finset α) (p : ↥s → Prop) : (∀ (x : ↥s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩

theorem Finset.exists_coe {α : Type u_4} (s : Finset α) (p : ↥s → Prop) : (∃ (x : ↥s), p x) ↔ ∃ (x : α), ∃ (h : x ∈ s), p ⟨x, h⟩

instance Finset.PiFinsetCoe.canLift (ι : Type u_4) (α : ι → Type u_5) [_ne : ∀ (i : ι), Nonempty (α i)] (s : Finset ι) : CanLift ((i : ↥s) → α ↑i) ((i : ι) → α i) (fun (f : (i : ι) → α i) (i : ↥s) => f ↑i) fun (x : (i : ↥s) → α ↑i) => True

instance Finset.PiFinsetCoe.canLift' (ι : Type u_4) (α : Type u_5) [_ne : Nonempty α] (s : Finset ι) : CanLift (↥s → α) (ι → α) (fun (f : ι → α) (i : ↥s) => f ↑i) fun (x : ↥s → α) => True

instance Finset.FinsetCoe.canLift {α : Type u_1} (s : Finset α) : CanLift α (↥s) Subtype.val fun (a : α) => a ∈ s

theorem Finset.coe_sort_coe {α : Type u_1} (s : Finset α) : ↑↑s = ↥s

Subset and strict subset relations

@[deprecated "This is now a syntactic identity" (since := "2026-05-24")]

theorem Finset.subset_of_le {α : Type u_1} {s t : Finset α} : s ⊆ t → s ⊆ t

theorem Finset.subset_def {α : Type u_1} {s t : Finset α} : s ⊆ t ↔ s.val ⊆ t.val

theorem Finset.ssubset_def {α : Type u_1} {s t : Finset α} : s ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s

theorem Finset.Subset.refl {α : Type u_1} (s : Finset α) : s ⊆ s

theorem Finset.Subset.rfl {α : Type u_1} {s : Finset α} : s ⊆ s

theorem Finset.subset_of_eq {α : Type u_1} {s t : Finset α} (h : s = t) : s ⊆ t

theorem Finset.Subset.trans {α : Type u_1} {s₁ s₂ s₃ : Finset α} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃

theorem Finset.Superset.trans {α : Type u_1} {s₁ s₂ s₃ : Finset α} : s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃

theorem Finset.mem_of_subset {α : Type u_1} {s₁ s₂ : Finset α} {a : α} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂

theorem Finset.notMem_mono {α : Type u_1} {s t : Finset α} (h : s ⊆ t) {a : α} : ¬a ∈ t → ¬a ∈ s

theorem Finset.not_mem_subset {α : Type u_1} {s t : Finset α} (h : s ⊆ t) {a : α} : ¬a ∈ t → ¬a ∈ s

Alias of Finset.notMem_mono.

theorem Finset.Subset.antisymm {α : Type u_1} {s₁ s₂ : Finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂

theorem Finset.subset_iff {α : Type u_1} {s₁ s₂ : Finset α} : s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂

theorem Finset.subset_iff_notMem {α : Type u_1} {s t : Finset α} : s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

theorem Finset.coe_subset {α : Type u_1} {s₁ s₂ : Finset α} : ↑s₁ ⊆ ↑s₂ ↔ s₁ ⊆ s₂

@[simp]

theorem Finset.val_le_iff {α : Type u_1} {s₁ s₂ : Finset α} : s₁.val ≤ s₂.val ↔ s₁ ⊆ s₂

theorem Finset.Subset.antisymm_iff {α : Type u_1} {s₁ s₂ : Finset α} : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁

theorem Finset.not_subset {α : Type u_1} {s t : Finset α} : ¬s ⊆ t ↔ ∃ (x : α), x ∈ s ∧ ¬x ∈ t

@[deprecated "This is now a syntactic equality" (since := "2026-05-24")]

theorem Finset.le_eq_subset {α : Type u_1} : (fun (x1 x2 : Finset α) => x1 ⊆ x2) = fun (x1 x2 : Finset α) => x1 ⊆ x2

@[deprecated "This is now a syntactic equality" (since := "2026-05-24")]

theorem Finset.lt_eq_subset {α : Type u_1} : (fun (x1 x2 : Finset α) => x1 ⊂ x2) = fun (x1 x2 : Finset α) => x1 ⊂ x2

@[deprecated "This is now a syntactic equality" (since := "2026-05-24")]

theorem Finset.le_iff_subset {α : Type u_1} {s₁ s₂ : Finset α} : s₁ ⊆ s₂ ↔ s₁ ⊆ s₂

@[deprecated "This is now a syntactic equality" (since := "2026-05-24")]

theorem Finset.lt_iff_ssubset {α : Type u_1} {s₁ s₂ : Finset α} : s₁ ⊂ s₂ ↔ s₁ ⊂ s₂

theorem Finset.coe_ssubset {α : Type u_1} {s₁ s₂ : Finset α} : ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂

@[simp]

theorem Finset.val_lt_iff {α : Type u_1} {s₁ s₂ : Finset α} : s₁.val < s₂.val ↔ s₁ ⊂ s₂

theorem Finset.val_strictMono {α : Type u_1} : StrictMono val

theorem Finset.ssubset_iff_subset_ne {α : Type u_1} {s t : Finset α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t

theorem Finset.ssubset_iff_of_subset {α : Type u_1} {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁ ⊂ s₂ ↔ ∃ (x : α), x ∈ s₂ ∧ ¬x ∈ s₁

theorem Finset.ssubset_of_ssubset_of_subset {α : Type u_1} {s₁ s₂ s₃ : Finset α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃

theorem Finset.ssubset_of_subset_of_ssubset {α : Type u_1} {s₁ s₂ s₃ : Finset α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) : s₁ ⊂ s₃

theorem Finset.exists_of_ssubset {α : Type u_1} {s₁ s₂ : Finset α} (h : s₁ ⊂ s₂) : ∃ (x : α), x ∈ s₂ ∧ ¬x ∈ s₁

instance Finset.isWellFounded_ssubset {α : Type u_1} : IsWellFounded (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

instance Finset.wellFoundedLT {α : Type u_1} : WellFoundedLT (Finset α)

Order embedding from Finset α to Set α

def Finset.coeEmb {α : Type u_1} : Finset α ↪o Set α

Coercion to Set α as an OrderEmbedding.

Equations

• Finset.coeEmb = { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Finset.coe_coeEmb {α : Type u_1} : ⇑coeEmb = SetLike.coe

Assorted results

These results can be defined using the current imports, but deserve to be given a nicer home.

@[implicit_reducible]

instance Finset.decidableDforallFinset {α : Type u_1} {s : Finset α} {p : (a : α) → a ∈ s → Prop} [_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] : Decidable (∀ (a : α) (h : a ∈ s), p a h)

Equations

• Finset.decidableDforallFinset = Multiset.decidableDforallMultiset

@[implicit_reducible]

instance Finset.instDecidableRelSubset {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

• x✝¹.instDecidableRelSubset x✝ = Finset.decidableDforallFinset

@[implicit_reducible]

instance Finset.instDecidableRelSSubset {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

• x✝¹.instDecidableRelSSubset x✝ = instDecidableAnd

@[implicit_reducible]

instance Finset.instDecidableLE {α : Type u_1} [DecidableEq α] : DecidableLE (Finset α)

Equations

• Finset.instDecidableLE = Finset.instDecidableRelSubset

@[implicit_reducible]

instance Finset.instDecidableLT {α : Type u_1} [DecidableEq α] : DecidableLT (Finset α)

Equations

• Finset.instDecidableLT = Finset.instDecidableRelSSubset

@[implicit_reducible]

instance Finset.decidableDExistsFinset {α : Type u_1} {s : Finset α} {p : (a : α) → a ∈ s → Prop} [_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] : Decidable (∃ (a : α), ∃ (h : a ∈ s), p a h)

Equations

• Finset.decidableDExistsFinset = Multiset.decidableDexistsMultiset

@[implicit_reducible]

instance Finset.decidableExistsAndFinset {α : Type u_1} {s : Finset α} {p : α → Prop} [_hp : (a : α) → Decidable (p a)] : Decidable (∃ (a : α), a ∈ s ∧ p a)

Equations

• Finset.decidableExistsAndFinset = decidable_of_iff (∃ (a : α), ∃ (x : a ∈ s), p a) ⋯

@[implicit_reducible]

instance Finset.decidableExistsAndFinsetCoe {α : Type u_1} {s : Finset α} {p : α → Prop} [DecidablePred p] : Decidable (∃ (a : α), a ∈ ↑s ∧ p a)

Equations

• Finset.decidableExistsAndFinsetCoe = Finset.decidableExistsAndFinset

@[implicit_reducible]

instance Finset.decidableEqPiFinset {α : Type u_1} {s : Finset α} {β : α → Type u_4} [_h : (a : α) → DecidableEq (β a)] : DecidableEq ((a : α) → a ∈ s → β a)

decidable equality for functions whose domain is bounded by finsets

Equations

• Finset.decidableEqPiFinset = Multiset.decidableEqPiMultiset

@[implicit_reducible]

instance List.instDecidableMapsToCoeFinsetOfDecidablePredMemSet {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} {t : Set β} [DecidablePred fun (x : β) => x ∈ t] : Decidable (Set.MapsTo f (↑s) t)

Equations

• List.instDecidableMapsToCoeFinsetOfDecidablePredMemSet = List.instDecidableMapsToCoeFinsetOfDecidablePredMemSet._aux_1

@[implicit_reducible]

instance List.instDecidableSurjOnCoeFinsetOfDecidableEq {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} {t' : Finset β} [DecidableEq β] : Decidable (Set.SurjOn f ↑s ↑t')

Equations

• List.instDecidableSurjOnCoeFinsetOfDecidableEq = List.instDecidableSurjOnCoeFinsetOfDecidableEq._aux_1

theorem Finset.pairwise_subtype_iff_pairwise_finset' {α : Type u_1} {β : Type u_2} {s : Finset α} (r : β → β → Prop) (f : α → β) : Pairwise (Function.onFun r fun (x : ↥s) => f ↑x) ↔ (↑s).Pairwise (Function.onFun r f)

theorem Finset.pairwise_subtype_iff_pairwise_finset {α : Type u_1} {s : Finset α} (r : α → α → Prop) : Pairwise (Function.onFun r fun (x : ↥s) => ↑x) ↔ (↑s).Pairwise r