Finite sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 amultiset α
of elements;nodup
is a proof thatval
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:
Lean refers to these operations as big_operator
s.
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 afinset
requires two pieces of data:val
, amultiset α
of elements, andnodup
, a proof thatval
has no duplicates.finset.has_mem
: Defines membershipa ∈ (s : finset α)
.finset.has_coe
: Provides a coercions : finset α
tos : set α
.finset.has_coe_to_sort
: Coerces : finset α
to the type of allx ∈ s
.finset.induction_on
: Induction on finsets. To prove a proposition about an arbitraryfinset α
, it suffices to prove it for the empty finset, and to show that if it holds for somefinset α
, then it holds for the finset obtained by inserting a new element.finset.choose
: Given a proofh
of existence and uniqueness of a certain element satisfying a predicate,choose s h
returns the element ofs
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 anyn : ℕ
,range n
is equal to{0, 1, ... , n - 1} ⊆ ℕ
. This convention is consistent with other languages and normalizescard (range n) = n
. Beware,n
is not inrange n
.finset.attach
: Givens : 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.filter
: Given a predicatep : α → Prop
,s.filter p
is the finset consisting of those elements ins
satisfying the predicatep
.
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
: Definess ∪ t
(ors ⊔ t
) as the union ofs
andt
. Seefinset.sup
/finset.bUnion
for finite unions.finset.has_inter
: Definess ∩ t
(ors ⊓ t
) as the intersection ofs
andt
. Seefinset.inf
for finite intersections.finset.disj_union
: Given a hypothesish
which states that finsetss
andt
are disjoint,s.disj_union t h
is the set such thata ∈ disj_union s t h
iffa ∈ s
ora ∈ t
; this does not require decidable equality on the typeα
.
Operations on two or more finsets #
insert
andfinset.cons
: For anya : α
,insert s a
returnss ∪ {a}
.cons s a h
returns the same except that it requires a hypothesis stating thata
is not already ins
. 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 anya : α
,erase s a
returnss
with the elementa
removed.finset.has_sdiff
: Defines the set differences \ t
for finsetss
andt
.finset.product
: Given finsets ofα
andβ
, defines finsets ofα × β
. For arbitrary dependent products, seedata.finset.pi
.finset.bUnion
: Finite unions of finsets; given an indexing functionf : α → finset β
and as : finset α
,s.bUnion f
is the union of all finsets of the formf a
fora ∈ s
.finset.bInter
: TODO: Implemement finite intersections.
Maps constructed using finsets #
finset.piecewise
: Given two functionsf
,g
,s.piecewise f g
is a function which is equal tof
ons
andg
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 sayings ≠ ∅
. 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 froms
tot
given thats ≃ t
. TODO: examples
Tags #
finite sets, finset
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.
Instances for finset
- finset.has_sizeof_inst
- multiset.can_lift_finset
- finset.has_mem
- finset.set.has_coe_t
- finset.has_coe_to_sort
- finset.has_subset
- finset.has_ssubset
- finset.partial_order
- finset.has_subset.subset.is_refl
- finset.has_subset.subset.is_trans
- finset.has_subset.subset.is_antisymm
- finset.has_ssubset.ssubset.is_irrefl
- finset.has_ssubset.ssubset.is_trans
- finset.has_ssubset.ssubset.is_asymm
- finset.has_ssubset.ssubset.is_nonstrict_strict_order
- finset.is_well_founded_ssubset
- finset.is_well_founded_lt
- finset.has_emptyc
- finset.inhabited_finset
- finset.order_bot
- finset.has_singleton
- finset.nontrivial'
- finset.unique
- finset.has_insert
- finset.is_lawful_singleton
- finset.has_union
- finset.has_inter
- finset.lattice
- finset.has_union.union.is_commutative
- finset.has_union.union.is_associative
- finset.has_union.union.is_idempotent
- finset.distrib_lattice
- finset.has_sdiff
- finset.generalized_boolean_algebra
- finset.has_sep
- finset.can_lift
- finset.bounded_order
- finset.boolean_algebra
- finset.infinite
- finset.fintype
- set.finite.can_lift
- finset.has_repr
- finset.smul_comm_class_finset
- finset.vadd_comm_class_finset
- finset.smul_comm_class_finset'
- finset.vadd_comm_class_finset'
- finset.smul_comm_class_finset''
- finset.vadd_comm_class_finset''
- finset.smul_comm_class
- finset.vadd_comm_class
- finset.is_scalar_tower
- finset.vadd_assoc_class
- finset.is_scalar_tower'
- finset.vadd_assoc_class'
- finset.is_scalar_tower''
- finset.vadd_assoc_class''
- finset.is_central_scalar
- finset.is_central_vadd
- finset.no_zero_divisors
- finset.no_zero_smul_divisors
- finset.no_zero_smul_divisors_finset
- finset.encodable
- finset.countable
- denumerable.finset
- equiv_functor_finset
- geometry.simplicial_complex.has_mem
- fin_enum.finset.fin_enum
- finset.locally_finite_order
- finset.functor
- finset.is_lawful_functor
- finset.has_pure
- finset.applicative
- finset.is_lawful_applicative
- finset.is_comm_applicative
- finset.monad
- finset.is_lawful_monad
- finset.alternative
Equations
- multiset.can_lift_finset = {prf := _}
Equations
- finset.has_decidable_eq s₁ s₂ = decidable_of_iff (s₁.val = s₂.val) finset.val_inj
membership #
Equations
set coercion #
Equations
extensionality #
type coercion #
Coercion from a finset to the corresponding subtype.
Equations
- finset.pi_finset_coe.can_lift ι α s = pi_subtype.can_lift ι α (λ (_x : ι), _x ∈ s)
Equations
- finset.pi_finset_coe.can_lift' ι α s = finset.pi_finset_coe.can_lift ι (λ (_x : ι), α) s
Subset and strict subset relations #
Equations
- finset.partial_order = {le := has_subset.subset finset.has_subset, lt := has_ssubset.ssubset finset.has_ssubset, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Coercion to set α
as an order_embedding
.
Equations
- finset.coe_emb = {to_embedding := {to_fun := coe coe_to_lift, inj' := _}, map_rel_iff' := _}
Nonempty #
The property s.nonempty
expresses the fact that the finset s
is not empty. It should be used
in theorem assumptions instead of ∃ x, x ∈ s
or s ≠ ∅
as it gives access to a nice API thanks
to the dot notation.
Instances for finset.nonempty
Equations
- finset.decidable_nonempty = decidable_of_iff (∃ (a : α) (H : a ∈ s), true) finset.decidable_nonempty._proof_1
Alias of the reverse direction of finset.coe_nonempty
.
Alias of the reverse direction of finset.nonempty_coe_sort
.
empty #
Equations
Equations
Alias of the reverse direction of finset.empty_ssubset
.
singleton #
{a} : finset a
is the set {a}
containing a
and nothing else.
This differs from insert a ∅
in that it does not require a decidable_eq
instance for α
.
Alias of the forward direction of finset.nonempty_iff_eq_singleton_default
.
A finset is nontrivial if it has at least two elements.
Equations
- s.nontrivial = ↑s.nontrivial
Equations
- finset.unique = {to_inhabited := {default := ∅}, uniq := _}
cons #
cons a s h
is the set {a} ∪ s
containing a
and the elements of s
. It is the same as
insert a s
when it is defined, but unlike insert a s
it does not require decidable_eq α
,
and the union is guaranteed to be disjoint.
disjoint #
disjoint union #
disj_union s t h
is the set such that a ∈ disj_union s t h
iff a ∈ s
or a ∈ t
.
It is the same as s ∪ t
, but it does not require decidable equality on the type. The hypothesis
ensures that the sets are disjoint.
insert #
insert a s
is the set {a} ∪ s
containing a
and the elements of s
.
Equations
- finset.has_insert = {insert := λ (a : α) (s : finset α), {val := multiset.ndinsert a s.val, nodup := _}}
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)
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.
To prove a proposition about S : finset α
,
it suffices to prove it for the empty finset
,
and to show that if it holds for some finset α ⊆ S
,
then it holds for the finset
obtained by inserting a new element of S
.
To prove a proposition about a nonempty s : finset α
, it suffices to show it holds for all
singletons and that if it holds for nonempty t : finset α
, then it also holds for the finset
obtained by inserting an element in t
.
Inserting an element to a finite set is equivalent to the option type.
Equations
- finset.subtype_insert_equiv_option h = {to_fun := λ (y : {i // i ∈ has_insert.insert x t}), dite (↑y = x) (λ (h : ↑y = x), option.none) (λ (h : ¬↑y = x), option.some ⟨↑y, _⟩), inv_fun := λ (y : option {i // i ∈ t}), option.elim ⟨x, _⟩ (λ (z : {i // i ∈ t}), ⟨↑z, _⟩) y, left_inv := _, right_inv := _}
Lattice structure #
Equations
- finset.lattice = {sup := has_union.union finset.has_union, le := partial_order.le finset.partial_order, lt := partial_order.lt finset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inter.inter finset.has_inter, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
- U.decidable_disjoint V = decidable_of_iff (∀ ⦃a : α⦄, a ∈ U → a ∉ V) _
union #
To prove a relation on pairs of finset X
, it suffices to show that it is
- symmetric,
- it holds when one of the
finset
s is empty, - it holds for pairs of singletons,
- if it holds for
[a, c]
and for[b, c]
, then it holds for[a ∪ b, c]
.
inter #
Equations
- finset.distrib_lattice = {sup := lattice.sup finset.lattice, le := lattice.le finset.lattice, lt := lattice.lt finset.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf finset.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
Alias of the reverse direction of finset.not_disjoint_iff_nonempty_inter
.
erase #
An element of s
that is not an element of erase s a
must be
a
.
sdiff #
Equations
- finset.generalized_boolean_algebra = {sup := distrib_lattice.sup finset.distrib_lattice, le := distrib_lattice.le finset.distrib_lattice, lt := distrib_lattice.lt finset.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf finset.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, sdiff := has_sdiff.sdiff finset.has_sdiff, bot := order_bot.bot finset.order_bot, sup_inf_sdiff := _, inf_inf_sdiff := _}
Symmetric difference #
attach #
piecewise #
decidable equality for functions whose domain is bounded by finsets
filter #
filter p s
is the set of elements of s
that satisfy p
.
Equations
- finset.filter p s = {val := multiset.filter p s.val, nodup := _}
If all elements of a finset
satisfy the predicate p
, s.filter p
is s
.
If all elements of a finset
fail to satisfy the predicate p
, s.filter p
is ∅
.
The following instance allows us to write {x ∈ s | p x}
for finset.filter p s
.
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 p s
. If p
happens to be decidable, the
simp-lemma finset.filter_congr_decidable
will make sure that finset.filter
uses the right
instance for decidability.
Equations
- finset.has_sep = {sep := λ (p : α → Prop) (x : finset α), finset.filter p x}
After filtering out everything that does not equal a given value, at most that value remains.
This is equivalent to filter_eq'
with the equality the other way.
After filtering out everything that does not equal a given value, at most that value remains.
This is equivalent to filter_eq
with the equality the other way.
range #
range n
is the set of natural numbers less than n
.
Equations
- finset.range n = {val := multiset.range n, nodup := _}
Useful in proofs by induction.
Equivalence between the set of natural numbers which are ≥ k
and ℕ
, given by n → n - k
.
dedup on list and multiset #
to_finset l
removes duplicates from the list l
to produce a finset.
disj_Union #
This section is about the bounded union of a disjoint indexed family t : α → finset β
of finite
sets over a finite set s : finset α
. In most cases finset.bUnion
should be preferred.
disj_Union s f h
is the set such that a ∈ disj_Union s f
iff a ∈ f i
for some i ∈ s
.
It is the same as s.bUnion f
, but it does not require decidable equality on the type. The
hypothesis ensures that the sets are disjoint.
Equations
- s.disj_Union t hf = {val := s.val.bind (finset.val ∘ t), nodup := _}
bUnion #
This section is about the bounded union of an indexed family t : α → finset β
of finite sets
over a finite set s : finset α
.
bUnion s t
is the union of t x
over x ∈ s
.
(This was formerly bind
due to the monad structure on types with decidable_eq
.)
choose #
Given a finset l
and a predicate p
, associate to a proof that there is a unique element of
l
satisfying p
this unique element, as an element of the corresponding subtype.
Equations
- finset.choose_x p l hp = multiset.choose_x p l.val hp
Given a finset l
and a predicate p
, associate to a proof that there is a unique element of
l
satisfying p
this unique element, as an element of the ambient type.
Equations
- finset.choose p l hp = ↑(finset.choose_x p l hp)
Inhabited types are equivalent to option β
for some β
by identifying default α
with none
.
Equations
- equiv.sigma_equiv_option_of_inhabited α = ⟨{x // x ≠ inhabited.default}, {to_fun := λ (x : α), dite (x = inhabited.default) (λ (h : x = inhabited.default), option.none) (λ (h : ¬x = inhabited.default), option.some ⟨x, h⟩), inv_fun := option.elim inhabited.default coe, left_inv := _, right_inv := _}⟩