Finite sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines predicates for finite and infinite sets and provides
fintype
instances for many set constructions. It also proves basic facts
about finite sets and gives ways to manipulate set.finite
expressions.
Main definitions #
set.finite : set α → Prop
set.infinite : set α → Prop
set.to_finite
to proveset.finite
for aset
from afinite
instance.set.finite.to_finset
to noncomputably produce afinset
from aset.finite
proof. (Seeset.to_finset
for a computable version.)
Implementation #
A finite set is defined to be a set whose coercion to a type has a fintype
instance.
Since set.finite
is Prop
-valued, this is the mere fact that the fintype
instance
exists.
There are two components to finiteness constructions. The first is fintype
instances for each
construction. This gives a way to actually compute a finset
that represents the set, and these
may be accessed using set.to_finset
. This gets the finset
in the correct form, since otherwise
finset.univ : finset s
is a finset
for the subtype for s
. The second component is
"constructors" for set.finite
that give proofs that fintype
instances exist classically given
other set.finite
proofs. Unlike the fintype
instances, these do not use any decidability
instances since they do not compute anything.
Tags #
finite sets
A set is finite if there is a finset
with the same elements.
This is represented as there being a fintype
instance for the set
coerced to a type.
Note: this is a custom inductive type rather than nonempty (fintype s)
so that it won't be frozen as a local instance.
Instances for set.finite
Alias of the forward direction of set.finite_def
.
Constructor for set.finite
using a finite
instance.
Projection of set.finite
to its finite
instance.
This is intended to be used with dot notation.
See also set.finite.fintype
and set.finite.nonempty_fintype
.
A finite set coerced to a type is a fintype
.
This is the fintype
projection for a set.finite
.
Note that because finite
isn't a typeclass, this definition will not fire if it
is made into an instance
Finite sets can be lifted to finsets.
Equations
- set.finite.can_lift = {prf := _}
Alias of the reverse direction of set.not_infinite
.
See also finite_or_infinite
, fintype_or_infinite
.
Basic properties of set.finite.to_finset
#
Fintype instances #
Every instance here should have a corresponding set.finite
constructor in the next section.
Equations
Equations
- s.fintype_union t = fintype.of_finset (s.to_finset ∪ t.to_finset) _
Equations
- s.fintype_sep p = fintype.of_finset (finset.filter p s.to_finset) _
Equations
- s.fintype_inter t = fintype.of_finset (s.to_finset ∩ t.to_finset) _
A fintype
instance for set intersection where the left set has a fintype
instance.
Equations
- s.fintype_inter_of_left t = fintype.of_finset (finset.filter (λ (_x : α), _x ∈ t) s.to_finset) _
A fintype
instance for set intersection where the right set has a fintype
instance.
Equations
- s.fintype_inter_of_right t = fintype.of_finset (finset.filter (λ (_x : α), _x ∈ s) t.to_finset) _
A fintype
structure on a set defines a fintype
structure on its subset.
Equations
- s.fintype_subset h = _.mpr (s.fintype_inter_of_left t)
Equations
- s.fintype_diff t = fintype.of_finset (s.to_finset \ t.to_finset) _
Equations
- s.fintype_diff_left t = s.fintype_sep (λ (_x : α), _x ∈ tᶜ)
Equations
- set.fintype_Union f = fintype.of_finset (finset.univ.bUnion (λ (i : plift ι), (f i.down).to_finset)) _
A union of sets with fintype
structure over a set with fintype
structure has a fintype
structure.
Equations
- s.fintype_bUnion t H = fintype.of_finset (s.to_finset.attach.bUnion (λ (x : {x // x ∈ s.to_finset}), (t ↑x).to_finset)) _
Equations
- s.fintype_bUnion' t = fintype.of_finset (s.to_finset.bUnion (λ (x : ι), (t x).to_finset)) _
If s : set α
is a set with fintype
instance and f : α → set β
is a function such that
each f a
, a ∈ s
, has a fintype
structure, then s >>= f
has a fintype
structure.
Equations
- s.fintype_bind f H = s.fintype_bUnion f H
Equations
- s.fintype_bind' f = s.fintype_bUnion' f
Equations
- set.fintype_empty = fintype.of_finset ∅ set.fintype_empty._proof_1
Equations
- set.fintype_singleton a = fintype.of_finset {a} _
Equations
A fintype
instance for inserting an element into a set
using the
corresponding insert
function on finset
. This requires decidable_eq α
.
There is also set.fintype_insert'
when a ∈ s
is decidable.
Equations
- set.fintype_insert a s = fintype.of_finset (has_insert.insert a s.to_finset) _
A fintype
structure on insert a s
when inserting a new element.
Equations
- s.fintype_insert_of_not_mem h = fintype.of_finset {val := a ::ₘ s.to_finset.val, nodup := _} _
A fintype
structure on insert a s
when inserting a pre-existing element.
Equations
The set.fintype_insert
instance requires decidable equality, but when a ∈ s
is decidable for this particular a
we can still get a fintype
instance by using
set.fintype_insert_of_not_mem
or set.fintype_insert_of_mem
.
This instance pre-dates set.fintype_insert
, and it is less efficient.
When decidable_mem_of_fintype
is made a local instance, then this instance would
override set.fintype_insert
if not for the fact that its priority has been
adjusted. See Note [lower instance priority].
Equations
- set.fintype_insert' a s = dite (a ∈ s) (λ (h : a ∈ s), s.fintype_insert_of_mem h) (λ (h : a ∉ s), s.fintype_insert_of_not_mem h)
Equations
- s.fintype_image f = fintype.of_finset (finset.image f s.to_finset) _
If a function f
has a partial inverse and sends a set s
to a set with [fintype]
instance,
then s
has a fintype
structure as well.
Equations
- s.fintype_of_fintype_image I = fintype.of_finset {val := multiset.filter_map g (f '' s).to_finset.val, nodup := _} _
Equations
Equations
Equations
Equations
- set.fintype_le_nat n = _.mpr (_.mp (set.fintype_lt_nat (n + 1)))
This is not an instance so that it does not conflict with the one in src/order/locally_finite.
Equations
Equations
image2 f s t
is fintype
if s
and t
are.
Equations
- set.fintype_image2 f s t = _.mpr ((s ×ˢ t).fintype_image (λ (x : α × β), f x.fst x.snd))
Equations
- f.fintype_seq' s = f.fintype_seq s
Equations
Finset #
Gives a set.finite
for the finset
coerced to a set
.
This is a wrapper around set.to_finite
.
Finite instances #
There is seemingly some overlap between the following instances and the fintype
instances
in data.set.finite
. While every fintype
instance gives a finite
instance, those
instances that depend on fintype
or decidable
instances need an additional finite
instance
to be able to generally apply.
Some set instances do not appear here since they are consequences of others, for example
subtype.finite
for subsets of a finite type.
Constructors for set.finite
#
Every constructor here should have a corresponding fintype
instance in the previous section
(or in the fintype
module).
The implementation of these constructors ideally should be no more than set.to_finite
,
after possibly setting up some fintype
and classical decidable
instances.
Alias of the forward direction of set.finite_univ_iff
.
Properties #
If P
is some relation between terms of γ
and sets in γ
,
such that every finite set t : set γ
has some c : γ
related to it,
then there is a recursively defined sequence u
in γ
so u n
is related to the image of {0, 1, ..., n-1}
under u
.
(We use this later to show sequentially compact sets are totally bounded.)
Cardinality #
Infinite sets #
Alias of the reverse direction of set.infinite_coe_iff
.
Embedding of ℕ
into an infinite set.
Equations
Alias of the reverse direction of set.infinite_image_iff
.
Order properties #
A decreasing union distributes over finite intersection.
An increasing intersection distributes over finite union.
A finite set is bounded above.
A finite set is bounded below.
A finset is bounded above.
A finset is bounded below.