- 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
- unique.fintype
- fin_enum.fintype
- nonempty_fin_lin_ord.to_fintype
- is_simple_lattice.fintype
- fintype.subtype_of_fintype
- fin.fintype
- empty.fintype
- pempty.fintype
- unit.fintype
- punit.fintype
- bool.fintype
- units_int.fintype
- additive.fintype
- multiplicative.fintype
- units.fintype
- option.fintype
- sigma.fintype
- prod.fintype
- ulift.fintype
- sum.fintype
- list.subtype.fintype
- multiset.subtype.fintype
- finset.subtype.fintype
- finset_coe.fintype
- plift.fintype
- Prop.fintype
- subtype.fintype
- pi.fintype
- d_array.fintype
- array.fintype
- vector.fintype
- quotient.fintype
- finset.fintype
- psigma.fintype
- psigma.fintype_prop_left
- psigma.fintype_prop_right
- psigma.fintype_prop_prop
- set.fintype
- pfun_fintype
- equiv.fintype
- set.fintype_empty
- set.fintype_insert
- set.fintype_singleton
- set.fintype_pure
- set.fintype_univ
- set.fintype_union
- set.fintype_sep
- set.fintype_inter
- set.fintype_image
- set.fintype_range
- set.fintype_map
- set.fintype_Union
- set.fintype_bUnion'
- set.fintype_lt_nat
- set.fintype_le_nat
- set.fintype_prod
- set.fintype_image2
- set.fintype_bind'
- set.fintype_seq
- set.nat.fintype_Iio
- quotient_group.fintype
- quotient_add_group.fintype
- category_theory.discrete_fintype
- category_theory.discrete_hom_fintype
- free_group.subtype.fintype
- 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
- fintype_bot
- set.Ico_ℕ_fintype
- set.Ico_pnat_fintype
- set.Ico_ℤ_fintype
- matrix.fintype
- zmod.fintype
- composition_as_set_fintype
- composition_fintype
- roots_of_unity.fintype
- Fintype.fintype
- partition.fintype
- simple_graph.fintype
- simple_graph.edges_fintype
- simple_graph.incidence_set_fintype
- simple_graph.neighbor_set_fintype
- simple_graph.dart.fintype
- computability.Γ'.fintype
- turing.TM2to1.Γ'.fintype
- alg_hom.fintype
- alg_equiv.fintype
- affine.simplex.points_with_circumcenter_index.fintype
- dihedral.fintype
- lucas_lehmer.X.fintype
- truncated_witt_vector.fintype
- pgame.fintype_left_moves
- pgame.fintype_right_moves
- pgame.fintype_left_moves_of_aux
- pgame.fintype_right_moves_of_aux
Equations
- finset.order_top = {top := finset.univ _inst_1, le := partial_order.le finset.partial_order, lt := partial_order.lt finset.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}
Equations
- finset.boolean_algebra = {sup := distrib_lattice.sup finset.distrib_lattice, le := distrib_lattice.le finset.distrib_lattice, lt := distrib_lattice.lt finset.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf finset.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := order_top.top finset.order_top, le_top := _, bot := semilattice_inf_bot.bot finset.semilattice_inf_bot, bot_le := _, compl := λ (s : finset α), finset.univ \ s, sdiff := has_sdiff.sdiff finset.has_sdiff, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _}
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
- fintype.decidable_eq_equiv_fintype = λ (a b : α ≃ β), decidable_of_iff (a.to_fun = b.to_fun) _
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_left_inverse_fintype f g = show decidable (∀ (x : α), g (f x) = x), from fintype.decidable_forall_fintype
Equations
- fintype.decidable_right_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
If l
lists all the elements of α
without duplicates, then α ≃ fin (l.length)
.
There is (computably) a bijection between α
and fin n
where
n = card α
. 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.
Equations
- fintype.equiv_fin α = _.mpr (quot.rec_on_subsingleton finset.univ.val (λ (l : list α) (h : ∀ (x : α), x ∈ l) (nd : l.nodup), trunc.mk (fintype.equiv_fin_of_forall_mem_list h nd)) 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 := _}
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 _
Subsingleton types are fintypes (with zero or one terms).
Equations
- fintype.of_subsingleton a = {elems := {a}, complete := _}
Construct a finset enumerating a set s
, given a fintype
instance.
Equations
- s.to_finset = {val := multiset.map subtype.val finset.univ.val, nodup := _}
Equations
- fin.fintype n = {elems := finset.fin_range n, complete := _}
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
Equations
Equations
Equations
Equations
- units_int.fintype = {elems := {1, -1}, complete := units_int.fintype._proof_1}
Equations
Equations
Equations
Given a finset on α
, lift it to being a finset on option α
using option.some
and then insert option.none
.
Equations
- s.insert_none = {val := none ::ₘ multiset.map some s.val, nodup := _}
Equations
- option.fintype = {elems := finset.univ.insert_none, complete := _}
Equations
- sigma.fintype β = {elems := finset.univ.sigma (λ (_x : α), finset.univ), complete := _}
Equations
- prod.fintype α β = {elems := finset.univ.product finset.univ, complete := _}
Given that α × β
is a fintype, α
is also a fintype.
Equations
- fintype.fintype_prod_left = {elems := finset.image prod.fst (fintype.elems (α × β)), complete := _}
Given that α × β
is a fintype, β
is also a fintype.
Equations
- fintype.fintype_prod_right = {elems := finset.image prod.snd (fintype.elems (α × β)), complete := _}
Equations
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))
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
.
A fintype
with cardinality zero is (constructively) equivalent to pempty
.
Equations
Equations
Equations
A finset
of a subsingleton type has cardinality at most one.
Equations
A set on a fintype, when coerced to a type, is a fintype.
Equations
- set_fintype s = subtype.fintype (λ (x : α), x ∈ s)
An embedding from a fintype
to itself can be promoted to an equivalence.
Equations
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
- 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.equiv_fin α).rec_on_subsingleton (λ (eα : α ≃ fin (fintype.card α)), (fintype.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 fis 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.
Embedding of ℕ
into an infinite type.
Equations
- infinite.nat_embedding α = {to_fun := nat_embedding_aux α _inst_1, inj' := _}
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
, fintype.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: fintype.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)