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.fintype.card α
: Cardinality of a fintype. Equal tofinset.univ.card
.perms_of_finset s
: The finset of permutations of the finsets
.fintype.trunc_equiv_fin
: A fintypeα
is computably equivalent tofin (card α)
. Thetrunc
-free, noncomputable version isfintype.equiv_fin
.fintype.trunc_equiv_of_card_eq
fintype.equiv_of_card_eq
: Two fintypes of same cardinality are equivalent. See above.fin.equiv_iff_eq
:fin m ≃ fin n
iffm = n
.infinite α
: Typeclass saying that a type is infinite. Defined asfintype α → false
.not_finite
: Nofinite
type has aninfinite
instance.infinite.nat_embedding
: An embedding ofℕ
into an infinite type.
We also provide the following versions of the pigeonholes principle.
fintype.exists_ne_map_eq_of_card_lt
andis_empty_of_card_lt
: Finitely many pigeons and pigeonholes. Weak formulation.finite.exists_ne_map_eq_of_infinite
: Infinitely many pigeons in finitely many pigeonholes. Weak formulation.finite.exists_infinite_fiber
: Infinitely many pigeons in finitely many pigeonholes. Strong formulation.
Some more pigeonhole-like statements can be found in data.fintype.card_embedding
.
Instances #
Among others, we provide fintype
instances for
- A
subtype
of a fintype. Seefintype.subtype
. - The
option
of a fintype. - The product of two fintypes.
- The sum of two fintypes.
Prop
.
and infinite
instances for
along with some machinery
- Types which have a surjection from/an injection to a
fintype
are themselves fintypes. Seefintype.of_injective
andfintype.of_surjective
. - Types which have an injection from/a surjection to an
infinite
type are themselvesinfinite
. Seeinfinite.of_injective
andinfinite.of_surjective
.
- elems : finset α
- complete : ∀ (x : α), x ∈ fintype.elems α
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 of this typeclass
- unique.fintype
- fintype.of_is_empty
- set.fintype_insert'
- nonempty_fin_lin_ord.to_fintype
- fin_enum.fintype
- set_like.fintype
- is_simple_order.fintype
- fin.fintype
- fintype.subtype_eq
- fintype.subtype_eq'
- unit.fintype
- punit.fintype
- bool.fintype
- units_int.fintype
- additive.fintype
- multiplicative.fintype
- option.fintype
- sigma.fintype
- prod.fintype
- ulift.fintype
- plift.fintype
- order_dual.fintype
- lex.fintype
- sum.fintype
- finset.fintype_coe_sort
- list.subtype.fintype
- multiset.subtype.fintype
- finset.subtype.fintype
- finset_coe.fintype
- plift.fintype_Prop
- Prop.fintype
- subtype.fintype
- units.fintype
- pi.fintype
- d_array.fintype
- array.fintype
- vector.fintype
- quotient.fintype
- finset.fintype
- function.embedding.fintype
- sym.sym'.fintype
- sym.fintype
- psigma.fintype
- psigma.fintype_prop_left
- psigma.fintype_prop_right
- psigma.fintype_prop_prop
- set.fintype
- pfun_fintype
- equiv.fintype
- set.fintype_univ
- set.fintype_union
- set.fintype_sep
- set.fintype_inter
- set.fintype_inter_of_left
- set.fintype_inter_of_right
- set.fintype_diff
- set.fintype_diff_left
- set.fintype_Union
- set.fintype_sUnion
- set.fintype_bUnion'
- set.fintype_bind'
- set.fintype_empty
- set.fintype_singleton
- set.fintype_pure
- set.fintype_insert
- set.fintype_image
- set.fintype_range
- set.fintype_map
- set.fintype_lt_nat
- set.fintype_le_nat
- set.fintype_prod
- set.fintype_image2
- set.fintype_seq
- set.fintype_seq'
- set.fintype_mem_finset
- conj_classes.fintype
- conjugates_of.fintype
- conj_classes.carrier.fintype
- subgroup.fintype
- add_subgroup.fintype
- subgroup.fintype_bot
- add_subgroup.fintype_bot
- monoid_hom.fintype_mrange
- add_monoid_hom.fintype_mrange
- monoid_hom.fintype_range
- add_monoid_hom.fintype_range
- ring_hom.fintype_srange
- ring_hom.fintype_range
- linear_map.fintype_range
- set.fintype_Icc
- set.fintype_Ico
- set.fintype_Ioc
- set.fintype_Ioo
- set.fintype_Ici
- set.fintype_Ioi
- set.fintype_Iic
- set.fintype_Iio
- quotient_group.fintype_quotient_right_rel
- quotient_add_group.fintype_quotient_right_rel
- quotient_group.fintype
- quotient_add_group.fintype
- alg_hom.fintype_range
- zmod.fintype
- fintype_nodup_list
- cycle.fintype_nodup_cycle
- cycle.fintype_nodup_nontrivial_cycle
- polynomial.root_set_fintype
- is_noetherian.basis.of_vector_space_index.fintype
- finite_dimensional.basis.of_vector_space_index.fintype
- composition_as_set_fintype
- composition_fintype
- nat.partition.fintype
- equiv.perm.vectors_prod_eq_one.fintype
- subgroup.fintype_quotient_normal_core
- minpoly.alg_hom.fintype
- ring_hom.fintype_field_range
- matrix.fintype
- category_theory.discrete_fintype
- category_theory.discrete_hom_fintype
- category_theory.fin_category.fintype_obj
- category_theory.fin_category.fintype_hom
- category_theory.limits.fintype_walking_parallel_pair
- category_theory.limits.walking_parallel_pair_hom.fintype
- category_theory.limits.wide_pullback_shape.fintype_obj
- category_theory.limits.wide_pullback_shape.fintype_hom
- category_theory.limits.wide_pushout_shape.fintype_obj
- category_theory.limits.wide_pushout_shape.fintype_hom
- category_theory.limits.fintype_walking_pair
- free_group.subtype.fintype
- abelianization.fintype
- module.free.choose_basis_index.fintype
- conj_act.fintype
- alg_equiv.fintype
- sign_type.fintype
- roots_of_unity.fintype
- category_theory.fin_bicone
- category_theory.fin_bicone_hom
- algebraic_geometry.Scheme.J.fintype
- simplicial_object.splitting.index_set.fintype
- module.End.eigenvalues.fintype
- Fintype.fintype
- category_theory.Mat_.F
- hall_matchings_on.fintype
- rel.image.fintype
- configuration.dual.fintype
- derangements.fintype
- simple_graph.fintype
- simple_graph.edges_fintype
- simple_graph.dart.fintype
- simple_graph.incidence_set_fintype
- simple_graph.neighbor_set_fintype
- simple_graph.subgraph.finite_at
- simple_graph.subgraph.neighbor_set.fintype
- simple_graph.subgraph.coe_finite_at
- simple_graph.fintype_set_walk_length
- finpartition.fintype
- simple_graph.coloring.fintype
- computability.Γ.fintype
- computability.Γ'.fintype
- turing.TM2to1.Γ'.fintype
- turing.partrec_to_TM2.Γ'.fintype
- set_of.fintype
- multiset.fintype_coe
- polynomial.gal.fintype
- galois_field.fintype
- affine.simplex.points_with_circumcenter_index.fintype
- sylow.fintype
- has_quotient.quotient.fintype
- alternating_group.fintype
- dihedral_group.fintype
- quaternion_group.fintype
- hamming.fintype
- class_group.fintype
- function_field.ring_of_integers.class_group.fintype
- number_field.embeddings.ring_hom.fintype
- number_field.ring_of_integers.class_group.fintype
- lucas_lehmer.X.fintype
- FinPartialOrder.is_fintype
- FinBoolAlg.is_fintype
- truncated_witt_vector.fintype
- pgame.fintype_left_moves
- pgame.fintype_right_moves
- pgame.fintype_left_moves_of_state_aux
- pgame.fintype_right_moves_of_state_aux
- alexandroff.fintype
- discrete_quotient.fintype
Instances of other typeclasses for fintype
- fintype.has_sizeof_inst
- fintype.subsingleton
- equiv_functor_fintype
Equations
- finset.order_top = {top := finset.univ _inst_1, le_top := _}
Note this is a special case of (finset.image_preimage f univ _).symm
.
A special case of finset.sup_eq_supr
that omits the useless x ∈ univ
binder.
A special case of finset.inf_eq_infi
that omits the useless x ∈ univ
binder.
Equations
- fintype.decidable_pi_fintype = λ (f g : Π (a : α), β a), decidable_of_iff (∀ (a : α), a ∈ fintype.elems α → f a = g a) _
Equations
- fintype.decidable_forall_fintype = decidable_of_iff (∀ (a : α), a ∈ finset.univ → p a) fintype.decidable_forall_fintype._proof_1
Equations
- fintype.decidable_exists_fintype = decidable_of_iff (∃ (a : α) (H : a ∈ finset.univ), p a) fintype.decidable_exists_fintype._proof_1
Equations
Equations
- fintype.decidable_eq_equiv_fintype = λ (a b : α ≃ β), decidable_of_iff (a.to_fun = b.to_fun) _
Equations
- fintype.decidable_eq_embedding_fintype = λ (a b : α ↪ β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_one_hom_fintype = λ (a b : one_hom α β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_zero_hom_fintype = λ (a b : zero_hom α β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_mul_hom_fintype = λ (a b : α →ₙ* β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_add_hom_fintype = λ (a b : add_hom α β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_add_monoid_hom_fintype = λ (a b : α →+ β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_monoid_hom_fintype = λ (a b : α →* β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_monoid_with_zero_hom_fintype = λ (a b : α →*₀ β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_eq_ring_hom_fintype = λ (a b : α →+* β), decidable_of_iff (⇑a = ⇑b) _
Equations
- fintype.decidable_injective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype
Equations
- fintype.decidable_surjective_fintype = λ (x : α → β), _.mpr fintype.decidable_forall_fintype
Equations
- fintype.decidable_bijective_fintype = λ (x : α → β), _.mpr and.decidable
Equations
- fintype.decidable_right_inverse_fintype f g = show decidable (∀ (x : α), g (f x) = x), from fintype.decidable_forall_fintype
Equations
- fintype.decidable_left_inverse_fintype f g = show decidable (∀ (x : β), f (g x) = x), from fintype.decidable_forall_fintype
Construct a proof of fintype α
from a universal multiset
Construct a proof of fintype α
from a universal list
card α
is the number of elements in α
, defined when α
is a fintype.
Equations
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.equiv_fin
for the noncomputable version,
and fintype.trunc_equiv_fin_of_card_eq
and fintype.equiv_fin_of_card_eq
for an equiv α ≃ fin n
given fintype.card α = n
.
See fintype.trunc_fin_bijection
for a version without [decidable_eq α]
.
Equations
- fintype.trunc_equiv_fin α = _.mpr (quot.rec_on_subsingleton finset.univ.val (λ (l : list α) (h : ∀ (x : α), x ∈ l) (nd : l.nodup), trunc.mk (list.nodup.nth_le_equiv_of_forall_mem_list l nd h).symm) finset.mem_univ_val _)
There is (noncomputably) an equivalence between α
and fin (card α)
.
See fintype.trunc_equiv_fin
for the computable version,
and fintype.trunc_equiv_fin_of_card_eq
and fintype.equiv_fin_of_card_eq
for an equiv α ≃ fin n
given fintype.card α = n
.
Equations
- fintype.equiv_fin α = let _inst : decidable_eq α := classical.dec_eq α in (fintype.trunc_equiv_fin α).out
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.trunc_equiv_fin
for a version that gives an equivalence
given [decidable_eq α]
.
Equations
- fintype.trunc_fin_bijection α = id (quot.rec_on_subsingleton finset.univ.val (λ (l : list α) (h : ∀ (x : α), x ∈ l) (nd : l.nodup), trunc.mk (list.nodup.nth_le_bijection_of_forall_mem_list l nd h)) finset.mem_univ_val _)
Given a predicate that can be represented by a finset, the subtype associated to the predicate is a fintype.
Equations
- fintype.subtype s H = {elems := {val := multiset.pmap subtype.mk s.val _, nodup := _}, complete := _}
Construct a fintype from a finset with the same elements.
Equations
- fintype.of_finset s H = fintype.subtype s H
If f : α → β
is a bijection and α
is a fintype, then β
is also a fintype.
Equations
- fintype.of_bijective f H = {elems := finset.map {to_fun := f, inj' := _} finset.univ, complete := _}
If f : α → β
is a surjection and α
is a fintype, then β
is also a fintype.
Equations
- fintype.of_surjective f H = {elems := finset.image f finset.univ, complete := _}
The inverse of an hf : injective
function f : α → β
, of the type ↥(set.range f) → α
.
This is the computable version of function.inv_fun
that requires fintype α
and decidable_eq β
,
or the function version of applying (equiv.of_injective 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 α
.
Equations
- hf.inv_of_mem_range = λ (b : ↥(set.range f)), finset.choose (λ (a : α), f a = ↑b) finset.univ _
The inverse of an embedding f : α ↪ β
, of the type ↥(set.range f) → α
.
This is the computable version of function.inv_fun
that requires fintype α
and decidable_eq β
,
or the function version of applying (equiv.of_injective 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 α
.
Equations
- f.inv_of_mem_range b = _.inv_of_mem_range b
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.
Equations
- fintype.of_injective f H = let _inst : Π (p : Prop), decidable p := classical.dec in dite (nonempty α) (λ (hα : nonempty α), let _inst_2 : inhabited α := classical.inhabited_of_nonempty hα in fintype.of_surjective (function.inv_fun f) _) (λ (hα : ¬nonempty α), {elems := ∅, complete := _})
If f : α ≃ β
and α
is a fintype, then β
is also a fintype.
Equations
- fintype.of_equiv α f = fintype.of_bijective ⇑f _
If the cardinality of α
is n
, there is computably a bijection between α
and fin n
.
See fintype.equiv_fin_of_card_eq
for the noncomputable definition,
and fintype.trunc_equiv_fin
and fintype.equiv_fin
for the bijection α ≃ fin (card α)
.
Equations
- fintype.trunc_equiv_fin_of_card_eq h = trunc.map (λ (e : α ≃ fin (fintype.card α)), e.trans (fin.cast h).to_equiv) (fintype.trunc_equiv_fin α)
If the cardinality of α
is n
, there is noncomputably a bijection between α
and fin n
.
See fintype.trunc_equiv_fin_of_card_eq
for the computable definition,
and fintype.trunc_equiv_fin
and fintype.equiv_fin
for the bijection α ≃ fin (card α)
.
Equations
- fintype.equiv_fin_of_card_eq h = let _inst : decidable_eq α := classical.dec_eq α in (fintype.trunc_equiv_fin_of_card_eq h).out
Two fintype
s with the same cardinality are (computably) in bijection.
See fintype.equiv_of_card_eq
for the noncomputable version,
and fintype.trunc_equiv_fin_of_card_eq
and fintype.equiv_fin_of_card_eq
for
the specialization to fin
.
Equations
- fintype.trunc_equiv_of_card_eq h = (fintype.trunc_equiv_fin_of_card_eq h).bind (λ (e : α ≃ fin (fintype.card β)), trunc.map (λ (e' : β ≃ fin (fintype.card β)), e.trans e'.symm) (fintype.trunc_equiv_fin β))
Two fintype
s with the same cardinality are (noncomputably) in bijection.
See fintype.trunc_equiv_of_card_eq
for the computable version,
and fintype.trunc_equiv_fin_of_card_eq
and fintype.equiv_fin_of_card_eq
for
the specialization to fin
.
Equations
- fintype.equiv_of_card_eq h = let _inst : decidable_eq α := classical.dec_eq α, _inst_3 : decidable_eq β := classical.dec_eq β in (fintype.trunc_equiv_of_card_eq h).out
Any subsingleton type with a witness is a fintype (with one term).
Equations
- fintype.of_subsingleton a = {elems := {a}, complete := _}
Note: this lemma is specifically about fintype.of_subsingleton
. For a statement about
arbitrary fintype
instances, use either fintype.card_le_one_iff_subsingleton
or
fintype.card_unique
.
Note: this lemma is specifically about fintype.of_is_empty
. For a statement about
arbitrary fintype
instances, use finset.univ_eq_empty
.
Note: this lemma is specifically about fintype.of_is_empty
. For a statement about
arbitrary fintype
instances, use fintype.card_eq_zero_iff
.
Construct a finset enumerating a set s
, given a fintype
instance.
Equations
- s.to_finset = {val := multiset.map subtype.val finset.univ.val, nodup := _}
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.
Equations
Equations
- fin.fintype n = {elems := {val := ↑(list.fin_range n), nodup := _}, complete := _}
fin
as a map from ℕ
to Type
is injective. Note that since this is a statement about
equality of types, using it should be avoided if possible.
Embed fin n
into fin (n + 1)
by appending a new fin.last n
to the univ
Short-circuit instance to decrease search for unique.fintype
,
since that relies on a subsingleton elimination for unique
.
Equations
- fintype.subtype_eq y = fintype.subtype {y} _
Short-circuit instance to decrease search for unique.fintype
,
since that relies on a subsingleton elimination for unique
.
Equations
- fintype.subtype_eq' y = fintype.subtype {y} _
Equations
Equations
- punit.fintype = fintype.of_subsingleton punit.star
Equations
- units_int.fintype = {elems := {1, -1}, complete := units_int.fintype._proof_1}
Equations
Equations
Equations
- option.fintype = {elems := ⇑finset.insert_none finset.univ, complete := _}
If option α
is a fintype
then so is α
Equations
- fintype_of_option = {elems := ⇑finset.erase_none (fintype.elems (option α)), complete := _}
Equations
- sigma.fintype β = {elems := finset.univ.sigma (λ (_x : α), finset.univ), complete := _}
Equations
- prod.fintype α β = {elems := finset.univ ×ˢ finset.univ, complete := _}
Given that α × β
is a fintype, α
is also a fintype.
Equations
- fintype.prod_left = {elems := finset.image prod.fst (fintype.elems (α × β)), complete := _}
Given that α × β
is a fintype, β
is also a fintype.
Equations
- fintype.prod_right = {elems := finset.image prod.snd (fintype.elems (α × β)), complete := _}
Equations
Equations
Equations
- order_dual.fintype α = _inst_1
Equations
- lex.fintype α = _inst_1
Equations
- sum.fintype α β = fintype.of_equiv (Σ (b : bool), cond b (ulift α) (ulift β)) ((equiv.sum_equiv_sigma_bool (ulift α) (ulift β)).symm.trans (equiv.ulift.sum_congr equiv.ulift))
Given that α ⊕ β
is a fintype, α
is also a fintype. This is non-computable as it uses
that sum.inl
is an injection, but there's no clear inverse if α
is empty.
Given that α ⊕ β
is a fintype, β
is also a fintype. This is non-computable as it uses
that sum.inr
is an injection, but there's no clear inverse if β
is empty.
Relation to finite
#
In this section we prove that α : Type*
is finite
if and only if fintype α
is nonempty.
The pigeonhole principle for finitely many pigeons and pigeonholes.
This is the fintype
version of finset.exists_ne_map_eq_of_card_lt_of_maps_to
.
Alias of the forward direction of finite.injective_iff_bijective
.
Alias of the forward direction of finite.surjective_iff_bijective
.
Alias of the forward direction of finite.injective_iff_surjective_of_equiv
.
Alias of the reverse direction of finite.injective_iff_surjective_of_equiv
.
Construct an equivalence from functions that are inverse to each other.
Construct an equivalence from functions that are inverse to each other.
Equations
Equations
Equations
Noncomputable equivalence between two finsets s
and t
as fintypes when there is a proof
that s.card = t.card
.
Equations
Equations
A set on a fintype, when coerced to a type, is a fintype.
Equations
- set_fintype s = subtype.fintype (λ (x : α), x ∈ s)
The αˣ
type is equivalent to a subtype of α × α
.
In a group_with_zero
α
, the unit group αˣ
is equivalent to the subtype of nonzero
elements.
Equations
- units.fintype = fintype.of_equiv {p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1} (units_equiv_prod_subtype α).symm
An embedding from a fintype
to itself can be promoted to an equivalence.
Equations
If ‖β‖ < ‖α‖
there are no embeddings α ↪ β
.
This is a formulation of the pigeonhole principle.
Note this cannot be an instance as it needs h
.
A constructive embedding of a fintype α
in another fintype β
when card α ≤ card β
.
Equations
- function.embedding.trunc_of_card_le h = (fintype.trunc_equiv_fin α).bind (λ (ea : α ≃ fin (fintype.card α)), trunc.map (λ (eb : β ≃ fin (fintype.card β)), ea.to_embedding.trans ((fin.cast_le h).to_embedding.trans eb.symm.to_embedding)) (fintype.trunc_equiv_fin β))
Given for all a : α
a finset t a
of δ a
, then one can define the
finset fintype.pi_finset t
of all functions taking values in t a
for all a
. This is the
analogue of finset.pi
where the base finset is univ
(but formally they are not the same, as
there is an additional condition i ∈ finset.univ
in the finset.pi
definition).
Equations
- fintype.pi_finset t = finset.map {to_fun := λ (f : Π (a : α), a ∈ finset.univ → δ a) (a : α), f a _, inj' := _} (finset.univ.pi t)
pi #
A dependent product of fintypes, indexed by a fintype, is a fintype.
Equations
- pi.fintype = {elems := fintype.pi_finset (λ (_x : α), finset.univ), complete := _}
Equations
- d_array.fintype = fintype.of_equiv (Π (i : fin n), α i) (equiv.d_array_equiv_fin α).symm
Equations
Equations
- vector.fintype = fintype.of_equiv (fin n → α) (equiv.vector_equiv_fin α n).symm
Equations
Equations
- finset.fintype = {elems := finset.univ.powerset, complete := _}
Equations
Equations
Equations
If two subtypes of a fintype have equal cardinality, so do their complements.
Equations
- psigma.fintype = fintype.of_equiv (Σ (i : α), β i) (equiv.psigma_equiv_sigma (λ (a : α), β a)).symm
Equations
- psigma.fintype_prop_right = fintype.of_equiv {a // β a} {to_fun := λ (_x : {a // β a}), psigma.fintype_prop_right._match_1 _x, inv_fun := λ (_x : Σ' (a : α), β a), psigma.fintype_prop_right._match_2 _x, left_inv := _, right_inv := _}
- psigma.fintype_prop_right._match_1 ⟨x, y⟩ = ⟨x, y⟩
- psigma.fintype_prop_right._match_2 ⟨x, y⟩ = ⟨x, y⟩
Equations
- set.fintype = {elems := finset.map {to_fun := coe coe_to_lift, inj' := _} finset.univ.powerset, complete := _}
An auxiliary function for quotient.fin_choice
. Given a
collection of setoids indexed by a type ι
, a (finite) list l
of
indices, and a function that for each i ∈ l
gives a term of the
corresponding quotient type, then there is a corresponding term in the
quotient of the product of the setoids indexed by l
.
Equations
- quotient.fin_choice_aux (i :: l) f = (f i _).lift_on₂ (quotient.fin_choice_aux l (λ (j : ι) (h : j ∈ l), f j _)) (λ (a : α i) (l_1 : Π (i : ι), i ∈ l → α i), ⟦(λ (j : ι) (h : j ∈ i :: l), dite (j = i) (λ (e : j = i), _.mpr a) (λ (e : ¬j = i), l_1 j _))⟧) _
- quotient.fin_choice_aux list.nil f = ⟦(λ (i : ι), false.elim)⟧
Given a collection of setoids indexed by a fintype ι
and a
function that for each i : ι
gives a term of the corresponding
quotient type, then there is corresponding term in the quotient of the
product of the setoids.
Equations
- quotient.fin_choice f = quotient.lift_on (quotient.rec_on finset.univ.val (λ (l : list ι), quotient.fin_choice_aux l (λ (i : ι) (_x : i ∈ l), f i)) _) (λ (f : Π (i : ι), i ∈ finset.univ.val → α i), ⟦(λ (i : ι), f i _)⟧) quotient.fin_choice._proof_2
Given a list, produce a list of all permutations of its elements.
Equations
- perms_of_list (a :: l) = perms_of_list l ++ l.bind (λ (b : α), list.map (λ (f : equiv.perm α), equiv.swap a b * f) (perms_of_list l))
- perms_of_list list.nil = [1]
Given a finset, produce the finset of all permutations of its elements.
Equations
- perms_of_finset s = quotient.hrec_on s.val (λ (l : list α) (hl : multiset.nodup ⟦l⟧), {val := ↑(perms_of_list l), nodup := _}) perms_of_finset._proof_2 _
The collection of permutations of a fintype is a fintype.
Equations
- fintype_perm = {elems := perms_of_finset finset.univ, complete := _}
Equations
- equiv.fintype = dite (fintype.card β = fintype.card α) (λ (h : fintype.card β = fintype.card α), (fintype.trunc_equiv_fin α).rec_on_subsingleton (λ (eα : α ≃ fin (fintype.card α)), (fintype.trunc_equiv_fin β).rec_on_subsingleton (λ (eβ : β ≃ fin (fintype.card β)), fintype.of_equiv (equiv.perm α) ((equiv.refl α).equiv_congr (eα.trans (h.rec_on eβ.symm)))))) (λ (h : ¬fintype.card β = fintype.card α), {elems := ∅, complete := _})
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.
Equations
- fintype.choose_x p hp = ⟨finset.choose p finset.univ _, _⟩
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 α
.
Equations
- fintype.choose p hp = ↑(fintype.choose_x p hp)
bij_inv f
is the unique inverse to a bijection f
. This acts
as a computable alternative to function.inv_fun
.
Equations
- fintype.bij_inv f_bij b = fintype.choose (λ (a : α), f a = b) _
A type is said to be infinite if it has no fintype instance.
Note that infinite α
is equivalent to is_empty (fintype α)
.
Instances of this typeclass
- char_zero.infinite
- denumerable.infinite
- is_alg_closed.infinite
- nat.infinite
- int.infinite
- infinite.set
- finset.infinite
- multiset.infinite
- list.infinite
- option.infinite
- sum.infinite_of_left
- sum.infinite_of_right
- prod.infinite_of_right
- prod.infinite_of_left
- zmod.infinite
- mv_polynomial.infinite_of_infinite
- mv_polynomial.infinite_of_nonempty
- polynomial.infinite
- set.Iio.infinite
- set.Iic.infinite
- set.Ioi.infinite
- set.Ici.infinite
- rat.infinite
- alexandroff.infinite
Alias of the forward direction of not_finite_iff_infinite
.
Alias of the reverse direction of not_finite_iff_infinite
.
Alias of the forward direction of not_infinite_iff_finite
.
Alias of the reverse direction of not_infinite_iff_finite
.
A non-infinite type is a fintype.
Equations
Any type is (classically) either a fintype
, or infinite
.
One can obtain the relevant typeclasses via cases fintype_or_infinite α; resetI
.
Equations
- fintype_or_infinite α = dite (infinite α) (λ (h : infinite α), psum.inr h) (λ (h : ¬infinite α), psum.inl (fintype_of_not_infinite h))
Embedding of ℕ
into an infinite type.
Equations
- infinite.nat_embedding α = {to_fun := nat_embedding_aux α _inst_1, inj' := _}
See infinite.exists_superset_card_eq
for a version that, for a s : finset α
,
provides a superset t : finset α
, s ⊆ t
such that t.card
is fixed.
The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the same pigeonhole.
See also: fintype.exists_ne_map_eq_of_card_lt
, finite.exists_infinite_fiber
.
The strong pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are infinitely many pigeons in finitely many pigeonholes, then there is a pigeonhole with infinitely many pigeons.
See also: finite.exists_ne_map_eq_of_infinite
For s : multiset α
, we can lift the existential statement that ∃ x, x ∈ s
to a trunc α
.
Equations
- trunc_of_multiset_exists_mem s = quotient.rec_on_subsingleton s (λ (l : list α) (h : ∃ (x : α), x ∈ ⟦l⟧), trunc_of_multiset_exists_mem._match_1 l h l h)
- trunc_of_multiset_exists_mem._match_1 l h (a :: _x) _x_1 = trunc.mk a
- trunc_of_multiset_exists_mem._match_1 l h list.nil _x = false.elim _
A fintype
with positive cardinality constructively contains an element.
Equations
- trunc_of_card_pos h = let _inst : nonempty α := _ in trunc_of_nonempty_fintype α
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
- trunc_sigma_of_exists h = trunc_of_nonempty_fintype (Σ' (a : α), P a)
A recursor principle for finite types, analogous to nat.rec
. It effectively says
that every fintype
is either empty
or option α
, up to an equiv
.
Equations
- fintype.trunc_rec_empty_option of_equiv h_empty h_option α = trunc.bind ((λ (n : ℕ), nat.rec ((fintype.trunc_equiv_of_card_eq fintype.trunc_rec_empty_option._proof_1).bind (λ (e : pempty ≃ ulift (fin 0)), trunc.mk (of_equiv e h_empty))) (λ (n : ℕ) (ih : trunc (P (ulift (fin n)))), (fintype.trunc_equiv_of_card_eq _).bind (λ (e : option (ulift (fin n)) ≃ ulift (fin n.succ)), trunc.map (λ (ih : P (ulift (fin n))), of_equiv e (h_option ih)) ih)) n) (fintype.card α)) (λ (h : P (ulift (fin (fintype.card α)))), trunc.map (λ (e : α ≃ fin (fintype.card α)), of_equiv (equiv.ulift.trans e.symm) h) (fintype.trunc_equiv_fin α))
An induction principle for finite types, analogous to nat.rec
. It effectively says
that every fintype
is either empty
or option α
, up to an equiv
.
An induction principle for finite types, analogous to nat.rec
. It effectively says
that every fintype
is either empty
or option α
, up to an equiv
.