Finite types #
This file defines a typeclass to state that a type is finite.
Main declarations #
Fintype α
: Typeclass saying that a type is finite. It takes as fields aFinset
and a proof that all terms of typeα
are in it.Finset.univ
: The finset of all elements of a fintype.
See Data.Fintype.Card
for the cardinality of a fintype,
the equivalence with Fin (Fintype.card α)
, and pigeonhole principles.
Instances #
Instances for Fintype
for
{x // p x}
are in this file asFintype.subtype
Option α
are inData.Fintype.Option
α × β
are inData.Fintype.Prod
α ⊕ β
are inData.Fintype.Sum
Σ (a : α), β a
are inData.Fintype.Sigma
These files also contain appropriate Infinite
instances for these types.
Infinite
instances for ℕ
, ℤ
, Multiset α
, and List α
are in Data.Fintype.Lattice
.
Types which have a surjection from/an injection to a Fintype
are themselves fintypes.
See Fintype.ofInjective
and Fintype.ofSurjective
.
- elems : Finset α
- complete : ∀ (x : α), x ∈ Fintype.elems
A proof that
elems
contains every element of the type
Fintype α
means that α
is finite, i.e. there are only
finitely many distinct elements of type α
. The evidence of this
is a finset elems
(a list up to permutation without duplicates),
together with a proof that everything of type α
is in the list.
Instances
Note this is a special case of (Finset.image_preimage f univ _).symm
.
Construct a proof of Fintype α
from a universal multiset
Instances For
Construct a proof of Fintype α
from a universal list
Instances For
If f : α → β
is a bijection and α
is a fintype, then β
is also a fintype.
Instances For
If f : α → β
is a surjection and α
is a fintype, then β
is also a fintype.
Instances For
The inverse of an hf : injective
function f : α → β
, of the type ↥(Set.range f) → α
.
This is the computable version of Function.invFun
that requires Fintype α
and DecidableEq β
,
or the function version of applying (Equiv.ofInjective f hf).symm
.
This function should not usually be used for actual computation because for most cases,
an explicit inverse can be stated that has better computational properties.
This function computes by checking all terms a : α
to find the f a = b
, so it is O(N) where
N = Fintype.card α
.
Instances For
The inverse of an embedding f : α ↪ β
, of the type ↥(Set.range f) → α
.
This is the computable version of Function.invFun
that requires Fintype α
and DecidableEq β
,
or the function version of applying (Equiv.ofInjective f f.injective).symm
.
This function should not usually be used for actual computation because for most cases,
an explicit inverse can be stated that has better computational properties.
This function computes by checking all terms a : α
to find the f a = b
, so it is O(N) where
N = Fintype.card α
.
Instances For
Given an injective function to a fintype, the domain is also a fintype. This is noncomputable because injectivity alone cannot be used to construct preimages.
Instances For
Any subsingleton type with a witness is a fintype (with one term).
Instances For
Note: this lemma is specifically about Fintype.of_isEmpty
. For a statement about
arbitrary Fintype
instances, use Finset.univ_eq_empty
.
Many Fintype
instances for sets are defined using an extensionally equal Finset
.
Rewriting s.toFinset
with Set.toFinset_ofFinset
replaces the term with such a Finset
.
Membership of a set with a Fintype
instance is decidable.
Using this as an instance leads to potential loops with Subtype.fintype
under certain decidability
assumptions, so it should only be declared a local instance.
Instances For
Alias of the reverse direction of Set.toFinset_subset_toFinset
.
Alias of the reverse direction of Set.toFinset_ssubset_toFinset
.
Embed Fin n
into Fin (n + 1)
by appending a new Fin.last n
to the univ
Embed Fin n
into Fin (n + 1)
by inserting
around a specified pivot p : Fin (n + 1)
into the univ
Short-circuit instance to decrease search for Unique.fintype
,
since that relies on a subsingleton elimination for Unique
.
Short-circuit instance to decrease search for Unique.fintype
,
since that relies on a subsingleton elimination for Unique
.
Given that α × β
is a fintype, α
is also a fintype.
Instances For
Given that α × β
is a fintype, β
is also a fintype.
Instances For
A set on a fintype, when coerced to a type, is a fintype.
Instances For
In a GroupWithZero
α
, the unit group αˣ
is equivalent to the subtype of nonzero
elements.
Instances For
Given a fintype α
, finsetOrderIsoSet
is the order isomorphism between Finset α
and Set α
(all sets on a finite type are finite).
Instances For
Given a fintype α
and a predicate p
, associate to a proof that there is a unique element of
α
satisfying p
this unique element, as an element of the corresponding subtype.
Instances For
Given a fintype α
and a predicate p
, associate to a proof that there is a unique element of
α
satisfying p
this unique element, as an element of α
.
Instances For
bijInv f
is the unique inverse to a bijection f
. This acts
as a computable alternative to Function.invFun
.
Instances For
By iterating over the elements of a fintype, we can lift an existential statement ∃ a, P a
to Trunc (Σ' a, P a)
, containing data.
Instances For
Auxiliary definition to show exists_seq_of_forall_finset_exists
.
Equations
- seqOfForallFinsetExistsAux P r h x = Classical.choose (h (Finset.image (fun i => seqOfForallFinsetExistsAux P r h ↑i) Finset.univ))
Instances For
Induction principle to build a sequence, by adding one point at a time satisfying a given relation with respect to all the previously chosen points.
More precisely, Assume that, for any finite set s
, one can find another point satisfying
some relation r
with respect to all the points in s
. Then one may construct a
function f : ℕ → α
such that r (f m) (f n)
holds whenever m < n
.
We also ensure that all constructed points satisfy a given predicate P
.
Induction principle to build a sequence, by adding one point at a time satisfying a given symmetric relation with respect to all the previously chosen points.
More precisely, Assume that, for any finite set s
, one can find another point satisfying
some relation r
with respect to all the points in s
. Then one may construct a
function f : ℕ → α
such that r (f m) (f n)
holds whenever m ≠ n
.
We also ensure that all constructed points satisfy a given predicate P
.