Instances for finite types #
This file is a collection of basic Fintype
instances for types such as Fin
, Prod
and pi types.
Embed Fin n
into Fin (n + 1)
by appending a new Fin.last n
to the univ
Given that α × β
is a fintype, α
is also a fintype.
Equations
Instances For
Given that α × β
is a fintype, β
is also a fintype.
Equations
Instances For
Equations
By iterating over the elements of a fintype, we can lift an existential statement ∃ a, P a
to Trunc (Σ' a, P a)
, containing data.
Equations
Instances For
For functions on finite sets, they are bijections iff they map universes into universes.
Auxiliary definition to show exists_seq_of_forall_finset_exists
.
Equations
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
.