Finite sets
mathlib has several different models for finite sets, and it can be confusing when you're first getting used to them!
This file builds the basic theory of finset α
,
modelled as a multiset α
without duplicates.
It's "constructive" in the since that there is an underlying list of elements, although this is wrapped in a quotient by permutations, so anytime you actually use this list you're obligated to show you didn't depend on the ordering.
There's also the typeclass fintype α
(which asserts that there is some finset α
containing every term of type α
)
as well as the predicate finite
on s : set α
(which asserts nonempty (fintype s)
).
Equations
- finset.has_decidable_eq s₁ s₂ = decidable_of_iff (s₁.val = s₂.val) finset.val_inj
membership
Equations
set coercion
Equations
extensionality
subset
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 := _}
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.
empty
The empty finset
Equations
- finset.empty = {val := 0, nodup := _}
Equations
Equations
- finset.inhabited = {default := ∅}
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 α
.
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 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
.
Inserting an element to a finite set is equivalent to the option type.
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
lattice laws
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
- finset.semilattice_inf_bot = {bot := ∅, le := lattice.le finset.lattice, lt := lattice.lt finset.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := lattice.inf finset.lattice, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
- finset.semilattice_sup_bot = {bot := semilattice_inf_bot.bot finset.semilattice_inf_bot, le := semilattice_inf_bot.le finset.semilattice_inf_bot, lt := semilattice_inf_bot.lt finset.semilattice_inf_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup finset.lattice, le_sup_left := _, le_sup_right := _, sup_le := _}
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 := _}
erase
An element of s
that is not an element of erase s a
must be
a
.
sdiff
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 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.
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 := _}
Equivalence between the set of natural numbers which are ≥ k
and ℕ
, given by n → n - k
.
erase_dup on list and multiset
to_finset l
removes duplicates from the list l
to produce a finset.
map
When f
is an embedding of α
in β
and s
is a finset in α
, then s.map f
is the image
finset in β
. The embedding condition guarantees that there are no duplicates in the image.
Equations
- finset.map f s = {val := multiset.map ⇑f s.val, nodup := _}
Associate to an embedding f
from α
to β
the embedding that maps a finset to its image
under f
.
Equations
- finset.map_embedding f = {to_fun := finset.map f, inj' := _}
image
image f s
is the forward image of s
under f
.
Equations
- finset.image f s = (multiset.map f s.val).to_finset
Because finset.image
requires a decidable_eq
instances for the target type,
we can only construct a functor finset
when working classically.
Equations
- finset.functor = {map := λ (α β : Type u_1) (f : α → β) (s : finset α), finset.image f s, map_const := λ (α β : Type u_1), (λ (f : β → α) (s : finset β), finset.image f s) ∘ function.const β}
Given a finset s
and a predicate p
, s.subtype p
is the finset of subtype p
whose
elements belong to s
.
Equations
- finset.subtype p s = finset.map {to_fun := λ (x : {x // x ∈ finset.filter p s}), ⟨x.val, _⟩, inj' := _} (finset.filter p s).attach
s.subtype p
converts back to s.filter p
with
embedding.subtype
.
If all elements of a finset
satisfy the predicate p
,
s.subtype p
converts back to s
with embedding.subtype
.
If a finset
of a subtype is converted to the main type with
embedding.subtype
, all elements of the result have the property of
the subtype.
If a finset
of a subtype is converted to the main type with
embedding.subtype
, the result does not contain any value that does
not satisfy the property of the subtype.
If a finset
of a subtype is converted to the main type with
embedding.subtype
, the result is a subset of the set giving the
subtype.
card
card s
is the cardinality (number of elements) of s
.
Equations
- s.card = ⇑multiset.card s.val
Suppose that, given objects defined on all strict subsets of any finset s
, one knows how to
define an object on s
. Then one can inductively define an object on all finsets, starting from
the empty set and iterating. This can be used either to define data, or to prove properties.
Equations
- {val := s, nodup := nd}.strong_induction_on ih = s.strong_induction_on (λ (s : multiset α) (IH : Π (t : multiset α), t < s → Π (_a : t.nodup), p {val := t, nodup := _a}) (nd : s.nodup), ih {val := s, nodup := nd} (λ (_x : finset α), finset.strong_induction_on._match_1 s IH nd _x)) nd
- finset.strong_induction_on._match_1 s IH nd {val := t, nodup := nd'} = λ (ss : {val := t, nodup := nd'} ⊂