Documentation

Mathlib.Data.Finset.Defs

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:

val is a Multiset α of elements;
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:

∑ i ∈ (s : Finset α), f i;
∏ 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

Instances For

instance Multiset.canLiftFinset {α : Type u_4} :

CanLift (Multiset α) (Finset α) Finset.val Multiset.Nodup

Equations

⋯ = ⋯

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}

Instances For

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⟩

instance 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

Equations

⋯ = ⋯

instance 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

Equations

⋯ = ⋯

instance Finset.FinsetCoe.canLift {α : Type u_1} (s : Finset α) :

CanLift α { x : α // x ∈ s } Subtype.val fun (a : α) => a ∈ s

Equations

⋯ = ⋯

@[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 ⋯

instance Finset.instIsReflSubset {α : Type u_1} :

IsRefl (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

⋯ = ⋯

instance Finset.instIsTransSubset {α : Type u_1} :

IsTrans (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

⋯ = ⋯

instance Finset.instIsAntisymmSubset {α : Type u_1} :

IsAntisymm (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

Equations

⋯ = ⋯

instance Finset.instIsIrreflSSubset {α : Type u_1} :

IsIrrefl (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

⋯ = ⋯

instance Finset.instIsTransSSubset {α : Type u_1} :

IsTrans (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

⋯ = ⋯

instance Finset.instIsAsymmSSubset {α : Type u_1} :

IsAsymm (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

⋯ = ⋯

instance Finset.instIsNonstrictStrictOrderSubsetSSubset {α : Type u_1} :

IsNonstrictStrictOrder (Finset α) (fun (x1 x2 : Finset α) => x1 ⊆ x2) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

⋯ = ⋯

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₁

instance Finset.isWellFounded_ssubset {α : Type u_1} :

IsWellFounded (Finset α) fun (x1 x2 : Finset α) => x1 ⊂ x2

Equations

⋯ = ⋯

instance Finset.wellFoundedLT {α : Type u_1} :

WellFoundedLT (Finset α)

Equations

⋯ = ⋯

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' := ⋯ }

Instances For

@[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