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 in (s : finset α), f i;
2. ∏ i in (s : finset α), f i.

Lean refers to these operations as big_operators. More information can be found in algebra.big_operators.basic.

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 data.fintype.basic. 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 data.fintype.basic.

finset.card, the size of a finset is defined in data.finset.card. This is then used to define fintype.card, the size of a type.

Main declarations #

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.has_mem: Defines membership a ∈ (s : finset α).
• finset.has_coe: Provides a coercion s : finset α to s : set α.
• finset.has_coe_to_sort: Coerce s : finset α to the type of all x ∈ s.
• finset.induction_on: Induction on finsets. 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.
• finset.choose: Given a proof h of existence and uniqueness of a certain element satisfying a predicate, choose s h returns the element of s satisfying that predicate.

Finset constructions #

• singleton: Denoted by {a}; the finset consisting of one element.
• finset.empty: Denoted by ∅. The finset associated to any type consisting of no elements.
• finset.range: For any n : ℕ, range n is equal to {0, 1, ... , n - 1} ⊆ ℕ. This convention is consistent with other languages and normalizes card (range n) = n. Beware, n is not in range n.
• finset.attach: Given s : finset α, attach s forms a finset of elements of the subtype {a // a ∈ s}; in other words, it attaches elements to a proof of membership in the set.

Finsets from functions #

• finset.image: Given a function f : α → β, s.image f is the image finset in β.
• finset.map: Given an embedding f : α ↪ β, s.map f is the image finset in β.
• finset.filter: Given a predicate p : α → Prop, s.filter p is the finset consisting of those elements in s satisfying the predicate p.

The lattice structure on subsets of finsets #

There is a natural lattice structure on the subsets of a set. In Lean, we use lattice notation to talk about things involving unions and intersections. See order.lattice. For the lattice structure on finsets, ⊥ is called bot with ⊥ = ∅ and ⊤ is called top with ⊤ = univ.

• finset.has_subset: Lots of API about lattices, otherwise behaves exactly as one would expect.
• finset.has_union: Defines s ∪ t (or s ⊔ t) as the union of s and t. See finset.sup/finset.bUnion for finite unions.
• finset.has_inter: Defines s ∩ t (or s ⊓ t) as the intersection of s and t. See finset.inf for finite intersections.
• finset.disj_union: Given a hypothesis h which states that finsets s and t are disjoint, s.disj_union t h is the set such that a ∈ disj_union s t h iff a ∈ s or a ∈ t; this does not require decidable equality on the type α.

Operations on two or more finsets #

• insert and finset.cons: For any a : α, insert s a returns s ∪ {a}. cons s a h returns the same except that it requires a hypothesis stating that a is not already in s. This does not require decidable equality on the type α.
• finset.has_union: see "The lattice structure on subsets of finsets"
• finset.has_inter: see "The lattice structure on subsets of finsets"
• finset.erase: For any a : α, erase s a returns s with the element a removed.
• finset.has_sdiff: Defines the set difference s \ t for finsets s and t.
• finset.product: Given finsets of α and β, defines finsets of α × β. For arbitrary dependent products, see data.finset.pi.
• finset.bUnion: Finite unions of finsets; given an indexing function f : α → finset β and a s : finset α, s.bUnion f is the union of all finsets of the form f a for a ∈ s.
• finset.bInter: TODO: Implemement finite intersections.

Maps constructed using finsets #

• finset.piecewise: Given two functions f, g, s.piecewise f g is a function which is equal to f on s and g on the complement.

Predicates on finsets #

• disjoint: defined via the lattice structure on finsets; two sets are disjoint if their intersection is empty.
• finset.nonempty: A finset is nonempty if it has elements. This is equivalent to saying s ≠ ∅. TODO: Decide on the simp normal form.

Equivalences between finsets #

• The data.equiv files describe a general type of equivalence, so look in there for any lemmas. There is some API for rewriting sums and products from s to t given that s ≃ t. TODO: examples

Tags #

finite sets, finset

membership #

set coercion #

extensionality #

type coercion #

Subset and strict subset relations #

Order embedding from finset α to set α #

Nonempty #

empty #

singleton #

cons #

disjoint union #

insert #

The universe annotation is required for the following instance, possibly this is a bug in Lean. See leanprover.zulipchat.com/#narrow/stream/113488-general/topic/strange.20error.20(universe.20issue.3F)

Lattice structure #

union #