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.

Convert a finset to a set in the natural way.

singleton a is the set {a} containing a and nothing else.

insert a s is the set {a} ∪ s containing a and the elements of s.

To prove a proposition about an arbitrary finset α, it suffices to prove it for the empty finset, and to show that if it holds for some finset α, then it holds for the finset obtained by inserting a new element.

s ∪ t is the set such that a ∈ s ∪ t iff a ∈ s or a ∈ t.

s ∩ t is the set such that a ∈ s ∩ t iff a ∈ s and a ∈ t.

erase s a is the set s - {a}, that is, the elements of s which are not equal to a.

s \ t is the set consisting of the elements of s that are not in t.

attach s takes the elements of s and forms a new set of elements of the subtype {x // x ∈ s}.

decidable equality for functions whose domain is bounded by finsets

filter p s is the set of elements of s that satisfy p.

The following instance allows us to write { x ∈ s | p x } for finset.filter s p. Since the former notation requires us to define this for all propositions p, and finset.filter only works for decidable propositions, the notation { x ∈ s | p x } is only compatible with classical logic because it uses classical.prop_decidable. We don't want to redo all lemmas of finset.filter for has_sep.sep, so we make sure that simp unfolds the notation { x ∈ s | p x } to finset.filter s p. If p happens to be decidable, the simp-lemma filter_congr_decidable will make sure that finset.filter uses the right instance for decidability.

range n is the set of natural numbers less than n.

Construct an empty or singleton finset from an option

to_finset s removes duplicates from the multiset s to produce a finset.

to_finset l removes duplicates from the list l to produce a finset.

image f s is the forward image of s under f.

card s is the cardinality (number of elements) of s.

bind s t is the union of t x over x ∈ s

product s t is the set of pairs (a, b) such that a ∈ s and b ∈ t.

sigma s t is the set of dependent pairs ⟨a, b⟩ such that a ∈ s and b ∈ t a.

fold op b f s folds the commutative associative operation op over the f-image of s, i.e. fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b`.

Supremum of a finite set: sup {a, b, c} f = f a ⊔ f b ⊔ f c

Infimum of a finite set: inf {a, b, c} f = f a ⊓ f b ⊓ f c

sort s constructs a sorted list from the unordered set s. (Uses merge sort algorithm.)

Ico n m is the set of natural numbers n ≤ k < m.

Ico_ℤ l u is the set of integers l ≤ k < u.

The antidiagonal of a natural number n is the finset of pairs (i,j) such that i+j = n.

A pair (i,j) is contained in the antidiagonal of n if and only if i+j=n.

The cardinality of the antidiagonal of n is n+1.

The antidiagonal of 0 is the list [(0,0)]