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.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. There is also univ', the noncomputable partner to univ, which is defined to be α as a finset if α is finite, and the empty finset otherwise. 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.
• Finset.instMembershipFinset: Defines membership a ∈ (s : Finset α).
• Finset.instCoeTCFinsetSet: Provides a coercion s : Finset α to s : Set α.
• Finset.instCoeSortFinsetType: Coerce s : Finset α to the type of all x ∈ s.

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

theorem Multiset.canLiftFinset {α : Type u_4} : CanLift (Multiset α) (Finset α) Finset.val Multiset.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 Finset.val

@[simp]

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

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

Equations

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

membership

instance Finset.instMembership {α : Type u_1} : Membership α (Finset α)

Equations

• Finset.instMembership = { mem := fun (s : Finset α) (a : α) => a ∈ s.val }

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

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 ∈ s, ¬a = b) ↔ a ∉ s

@[simp]

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

set coercion

def Finset.toSet {α : Type u_1} (s : Finset α) : Set α

Convert a finset to a set in the natural way.

Equations

• ↑s = {a : α | a ∈ s}

instance Finset.instCoeTCSet {α : Type u_1} : CoeTC (Finset α) (Set α)

Convert a finset to a set in the natural way.

Equations

• Finset.instCoeTCSet = { coe := Finset.toSet }

@[simp]

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

@[simp]

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

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₂

@[simp]

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

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

type coercion

instance Finset.instCoeSortType {α : Type u} : CoeSort (Finset α) (Type u)

Coercion from a finset to the corresponding subtype.

Equations

• Finset.instCoeSortType = { coe := fun (s : Finset α) => { x : α // x ∈ s } }

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

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

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

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

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

@[simp]

theorem Finset.coe_sort_coe {α : Type u_1} (s : Finset α) : ↑↑s = { x : α // x ∈ s }

Subset and strict subset relations

instance Finset.instHasSubset {α : Type u_1} : HasSubset (Finset α)

Equations

• Finset.instHasSubset = { Subset := fun (s t : Finset α) => ∀ ⦃a : α⦄, a ∈ s → a ∈ t }

instance Finset.instHasSSubset {α : Type u_1} : HasSSubset (Finset α)

Equations

• Finset.instHasSSubset = { SSubset := fun (s t : Finset α) => s ⊆ t ∧ ¬t ⊆ s }

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

Equations

• Finset.partialOrder = PartialOrder.mk ⋯

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

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

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

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

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

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

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

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

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.not_mem_mono {α : Type u_1} {s t : Finset α} (h : s ⊆ t) {a : α} : a ∉ t → a ∉ s

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₂

@[simp]

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

theorem Finset.GCongr.coe_subset_coe {α : Type u_1} {s₁ s₂ : Finset α} : s₁ ⊆ s₂ → ↑s₁ ⊆ ↑s₂

Alias of the reverse direction of Finset.coe_subset.

@[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 ∈ s, x ∉ t

@[simp]

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

@[simp]

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

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

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

@[simp]

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 Finset.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 ∈ 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 ∈ s₂, x ∉ s₁

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

theorem 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 := Finset.toSet, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

Assorted results

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

theorem Finset.sizeOf_lt_sizeOf_of_mem {α : Type u_1} [SizeOf α] {x : α} {s : Finset α} (hx : x ∈ s) : sizeOf x < sizeOf s

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

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

Equations

• x✝.instDecidableRelSubset x = Finset.decidableDforallFinset

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

Equations

• x✝.instDecidableRelSSubset x = instDecidableAnd

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

Equations

• Finset.instDecidableLE = Finset.instDecidableRelSubset

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

Equations

• Finset.instDecidableLT = Finset.instDecidableRelSSubset

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

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

Equations

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

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

Equations

• Finset.decidableExistsAndFinsetCoe = Finset.decidableExistsAndFinset

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

instance List.instDecidableInjOnToSetOfDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq α] {f : α → β} {s : Finset α} [DecidableEq β] : Decidable (Set.InjOn f ↑s)

Equations

• List.instDecidableInjOnToSetOfDecidableEq = inferInstanceAs (Decidable (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y))

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

Equations

• List.instDecidableMapsToToSetOfDecidablePredMemSet = inferInstanceAs (Decidable (∀ x ∈ s, f x ∈ t))

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

Equations

• List.instDecidableSurjOnToSetOfDecidableEq = inferInstanceAs (Decidable (∀ x ∈ t', ∃ y ∈ s, f y = x))

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

Equations

• List.instDecidableBijOnToSetOfDecidableEq = inferInstanceAs (Decidable (Set.MapsTo f ↑s ↑t' ∧ Set.InjOn f ↑s ∧ Set.SurjOn f ↑s ↑t'))

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

theorem Finset.pairwise_subtype_iff_pairwise_finset {α : Type u_1} {s : Finset α} (r : α → α → Prop) : Pairwise (r on fun (x : { x : α // x ∈ s }) => ↑x) ↔ (↑s).Pairwise r