Equivalences between Fintype
, Fin
and Finite
#
This file defines the bijection between a Fintype α
and Fin (Fintype.card α)
, and uses this to
relate Fintype
with Finite
. From that we can derive properties of Finite
and Infinite
,
and show some instances of Infinite
.
Main declarations #
Fintype.truncEquivFin
: A fintypeα
is computably equivalent toFin (card α)
. TheTrunc
-free, noncomputable version isFintype.equivFin
.Fintype.truncEquivOfCardEq
Fintype.equivOfCardEq
: Two fintypes of same cardinality are equivalent. See above.Fin.equiv_iff_eq
:Fin m ≃ Fin n
iffm = n
.Infinite.natEmbedding
: An embedding ofℕ
into an infinite type.
Types which have an injection from/a surjection to an Infinite
type are themselves Infinite
.
See Infinite.of_injective
and Infinite.of_surjective
.
Instances #
We provide Infinite
instances for
There is (computably) an equivalence between α
and Fin (card α)
.
Since it is not unique and depends on which permutation
of the universe list is used, the equivalence is wrapped in Trunc
to
preserve computability.
See Fintype.equivFin
for the noncomputable version,
and Fintype.truncEquivFinOfCardEq
and Fintype.equivFinOfCardEq
for an equiv α ≃ Fin n
given Fintype.card α = n
.
See Fintype.truncFinBijection
for a version without [DecidableEq α]
.
Equations
Instances For
There is (noncomputably) an equivalence between α
and Fin (card α)
.
See Fintype.truncEquivFin
for the computable version,
and Fintype.truncEquivFinOfCardEq
and Fintype.equivFinOfCardEq
for an equiv α ≃ Fin n
given Fintype.card α = n
.
Equations
Instances For
There is (computably) a bijection between Fin (card α)
and α
.
Since it is not unique and depends on which permutation
of the universe list is used, the bijection is wrapped in Trunc
to
preserve computability.
See Fintype.truncEquivFin
for a version that gives an equivalence
given [DecidableEq α]
.
Equations
Instances For
If the cardinality of α
is n
, there is computably a bijection between α
and Fin n
.
See Fintype.equivFinOfCardEq
for the noncomputable definition,
and Fintype.truncEquivFin
and Fintype.equivFin
for the bijection α ≃ Fin (card α)
.
Equations
Instances For
If the cardinality of α
is n
, there is noncomputably a bijection between α
and Fin n
.
See Fintype.truncEquivFinOfCardEq
for the computable definition,
and Fintype.truncEquivFin
and Fintype.equivFin
for the bijection α ≃ Fin (card α)
.
Equations
Instances For
Two Fintype
s with the same cardinality are (computably) in bijection.
See Fintype.equivOfCardEq
for the noncomputable version,
and Fintype.truncEquivFinOfCardEq
and Fintype.equivFinOfCardEq
for
the specialization to Fin
.
Equations
Instances For
Two Fintype
s with the same cardinality are (noncomputably) in bijection.
See Fintype.truncEquivOfCardEq
for the computable version,
and Fintype.truncEquivFinOfCardEq
and Fintype.equivFinOfCardEq
for
the specialization to Fin
.
Equations
Instances For
Relation to Finite
#
In this section we prove that α : Type*
is Finite
if and only if Fintype α
is nonempty.
Construct an equivalence from functions that are inverse to each other.
Equations
Instances For
Construct an equivalence from functions that are inverse to each other.
Equations
Instances For
Alias of Function.Embedding.equivOfFiniteSelfEmbedding
.
An embedding from a Fintype
to itself can be promoted to an equivalence.
Equations
Instances For
Alias of Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding
.
A constructive embedding of a fintype α
in another fintype β
when card α ≤ card β
.
Equations
Instances For
Any type is (classically) either a Fintype
, or Infinite
.
One can obtain the relevant typeclasses via cases fintypeOrInfinite α
.
Equations
Instances For
If s : Set α
is a proper subset of α
and f : α → s
is injective, then α
is infinite.
If s : Set α
is a proper subset of α
and f : s → α
is surjective, then α
is infinite.
Alias of Infinite.exists_notMem_finset
.