mathlib documentation

data.fintype.basic

Finite types #

This file defines a typeclass to state that a type is finite.

Main declarations #

We also provide the following versions of the pigeonholes principle.

Some more pigeonhole-like statements can be found in data.fintype.card_embedding.

Instances #

Among others, we provide fintype instances for

and infinite instances for

along with some machinery

@[class]
structure fintype (α : Type u_4) :
Type u_4

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
Instances of other typeclasses for fintype
def finset.univ {α : Type u_1} [fintype α] :

univ is the universal finite set of type finset α implied from the assumption fintype α.

Equations
@[simp]
theorem finset.mem_univ {α : Type u_1} [fintype α] (x : α) :
@[simp]
theorem finset.mem_univ_val {α : Type u_1} [fintype α] (x : α) :
theorem finset.eq_univ_iff_forall {α : Type u_1} [fintype α] {s : finset α} :
s = finset.univ ∀ (x : α), x s
theorem finset.eq_univ_of_forall {α : Type u_1} [fintype α] {s : finset α} :
(∀ (x : α), x s)s = finset.univ
@[simp, norm_cast]
theorem finset.coe_univ {α : Type u_1} [fintype α] :
@[simp, norm_cast]
theorem finset.coe_eq_univ {α : Type u_1} [fintype α] {s : finset α} :
theorem finset.univ_nonempty {α : Type u_1} [fintype α] [nonempty α] :
theorem finset.univ_eq_empty_iff {α : Type u_1} [fintype α] :
@[simp]
theorem finset.univ_eq_empty {α : Type u_1} [fintype α] [is_empty α] :
@[simp]
theorem finset.univ_unique {α : Type u_1} [fintype α] [unique α] :
@[simp]
theorem finset.subset_univ {α : Type u_1} [fintype α] (s : finset α) :
@[protected, instance]
def finset.order_top {α : Type u_1} [fintype α] :
Equations
theorem finset.sdiff_eq_inter_compl {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :
s \ t = s t
theorem finset.compl_eq_univ_sdiff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.mem_compl {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :
a s a s
theorem finset.not_mem_compl {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :
a s a s
@[simp, norm_cast]
theorem finset.coe_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.compl_empty {α : Type u_1} [fintype α] [decidable_eq α] :
@[simp]
theorem finset.union_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.inter_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.compl_union {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :
(s t) = s t
@[simp]
theorem finset.compl_inter {α : Type u_1} [fintype α] [decidable_eq α] (s t : finset α) :
(s t) = s t
@[simp]
theorem finset.compl_erase {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :
@[simp]
theorem finset.compl_insert {α : Type u_1} [fintype α] {s : finset α} [decidable_eq α] {a : α} :
@[simp]
theorem finset.insert_compl_self {α : Type u_1} [fintype α] [decidable_eq α] (x : α) :
@[simp]
theorem finset.compl_filter {α : Type u_1} [fintype α] [decidable_eq α] (p : α → Prop) [decidable_pred p] [Π (x : α), decidable (¬p x)] :
theorem finset.compl_singleton {α : Type u_1} [fintype α] [decidable_eq α] (a : α) :
theorem finset.insert_inj_on' {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
set.inj_on (λ (a : α), has_insert.insert a s) s
theorem finset.image_univ_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq α] [fintype β] {f : β → α} (hf : function.surjective f) :
theorem finset.map_univ_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : β α} (hf : function.surjective f) :
@[simp]
theorem finset.map_univ_equiv {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : β α) :
@[simp]
theorem finset.univ_inter {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.inter_univ {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.piecewise_univ {α : Type u_1} [fintype α] [Π (i : α), decidable (i finset.univ)] {δ : α → Sort u_2} (f g : Π (i : α), δ i) :
theorem finset.piecewise_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) [Π (i : α), decidable (i s)] [Π (i : α), decidable (i s)] {δ : α → Sort u_2} (f g : Π (i : α), δ i) :
@[simp]
theorem finset.piecewise_erase_univ {α : Type u_1} [fintype α] {δ : α → Sort u_2} [decidable_eq α] (a : α) (f g : Π (a : α), δ a) :
theorem finset.univ_map_equiv_to_embedding {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (e : α β) :
@[simp]
theorem finset.univ_filter_exists {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) [fintype β] [decidable_pred (λ (y : β), ∃ (x : α), f x = y)] [decidable_eq β] :
finset.filter (λ (y : β), ∃ (x : α), f x = y) finset.univ = finset.image f finset.univ
theorem finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) [fintype β] [decidable_pred (λ (y : β), y set.range f)] [decidable_eq β] :

Note this is a special case of (finset.image_preimage f univ _).symm.

theorem finset.coe_filter_univ {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
(finset.filter p finset.univ) = {x : α | p x}
theorem finset.sup_univ_eq_supr {α : Type u_1} {β : Type u_2} [fintype α] [complete_lattice β] (f : α → β) :

A special case of finset.sup_eq_supr that omits the useless x ∈ univ binder.

theorem finset.inf_univ_eq_infi {α : Type u_1} {β : Type u_2} [fintype α] [complete_lattice β] (f : α → β) :

A special case of finset.inf_eq_infi that omits the useless x ∈ univ binder.

@[simp]
theorem finset.fold_inf_univ {α : Type u_1} [fintype α] [semilattice_inf α] [order_bot α] (a : α) :
@[simp]
theorem finset.fold_sup_univ {α : Type u_1} [fintype α] [semilattice_sup α] [order_top α] (a : α) :
@[protected, instance]
def fintype.decidable_pi_fintype {α : Type u_1} {β : α → Type u_2} [Π (a : α), decidable_eq (β a)] [fintype α] :
decidable_eq (Π (a : α), β a)
Equations
@[protected, instance]
def fintype.decidable_forall_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :
decidable (∀ (a : α), p a)
Equations
@[protected, instance]
def fintype.decidable_exists_fintype {α : Type u_1} {p : α → Prop} [decidable_pred p] [fintype α] :
decidable (∃ (a : α), p a)
Equations
@[protected, instance]
def fintype.decidable_mem_range_fintype {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α → β) :
decidable_pred (λ (_x : β), _x set.range f)
Equations
@[protected, instance]
def fintype.decidable_eq_equiv_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :
Equations
@[protected, instance]
def fintype.decidable_eq_embedding_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :
Equations
@[protected, instance]
def fintype.decidable_eq_one_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_one α] [has_one β] :
Equations
@[protected, instance]
def fintype.decidable_eq_zero_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_zero α] [has_zero β] :
Equations
@[protected, instance]
def fintype.decidable_eq_mul_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_mul α] [has_mul β] :
Equations
@[protected, instance]
def fintype.decidable_eq_add_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_add α] [has_add β] :
Equations
@[protected, instance]
def fintype.decidable_eq_add_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [add_zero_class α] [add_zero_class β] :
Equations
@[protected, instance]
def fintype.decidable_eq_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [mul_one_class α] [mul_one_class β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def fintype.decidable_eq_ring_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [semiring α] [semiring β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def fintype.decidable_right_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] (f : α → β) (g : β → α) :
Equations
@[protected, instance]
def fintype.decidable_left_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype β] (f : α → β) (g : β → α) :
Equations
def fintype.of_multiset {α : Type u_1} [decidable_eq α] (s : multiset α) (H : ∀ (x : α), x s) :

Construct a proof of fintype α from a universal multiset

Equations
def fintype.of_list {α : Type u_1} [decidable_eq α] (l : list α) (H : ∀ (x : α), x l) :

Construct a proof of fintype α from a universal list

Equations
def fintype.card (α : Type u_1) [fintype α] :

card α is the number of elements in α, defined when α is a fintype.

Equations
def fintype.trunc_equiv_fin (α : Type u_1) [decidable_eq α] [fintype α] :

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
noncomputable def fintype.equiv_fin (α : Type u_1) [fintype α] :

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
def fintype.trunc_fin_bijection (α : Type u_1) [fintype α] :

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
@[protected, instance]
def fintype.subsingleton (α : Type u_1) :
@[protected]
def fintype.subtype {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x s p x) :
fintype {x // p x}

Given a predicate that can be represented by a finset, the subtype associated to the predicate is a fintype.

Equations
theorem fintype.subtype_card {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x s p x) :
fintype.card {x // p x} = s.card
theorem fintype.card_of_subtype {α : Type u_1} {p : α → Prop} (s : finset α) (H : ∀ (x : α), x s p x) [fintype {x // p x}] :
fintype.card {x // p x} = s.card
def fintype.of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x s x p) :

Construct a fintype from a finset with the same elements.

Equations
@[simp]
theorem fintype.card_of_finset {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x s x p) :
theorem fintype.card_of_finset' {α : Type u_1} {p : set α} (s : finset α) (H : ∀ (x : α), x s x p) [fintype p] :
def fintype.of_bijective {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) (H : function.bijective f) :

If f : α → β is a bijection and α is a fintype, then β is also a fintype.

Equations
def fintype.of_surjective {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] (f : α → β) (H : function.surjective f) :

If f : α → β is a surjection and α is a fintype, then β is also a fintype.

Equations
def function.injective.inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) :
(set.range f) → α

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
theorem function.injective.left_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) (b : (set.range f)) :
@[simp]
theorem function.injective.right_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) (a : α) :
hf.inv_of_mem_range f a, _⟩ = a
theorem function.injective.inv_fun_restrict {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) [nonempty α] :
theorem function.injective.inv_of_mem_range_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (hf : function.injective f) :
def function.embedding.inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) (b : (set.range f)) :
α

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
@[simp]
theorem function.embedding.left_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) (b : (set.range f)) :
@[simp]
theorem function.embedding.right_inv_of_inv_of_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) (a : α) :
theorem function.embedding.inv_fun_restrict {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) [nonempty α] :
theorem function.embedding.inv_of_mem_range_surjective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) :
noncomputable def fintype.of_injective {α : Type u_1} {β : Type u_2} [fintype β] (f : α → β) (H : function.injective f) :

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
def fintype.of_equiv {β : Type u_2} (α : Type u_1) [fintype α] (f : α β) :

If f : α ≃ β and α is a fintype, then β is also a fintype.

Equations
theorem fintype.of_equiv_card {α : Type u_1} {β : Type u_2} [fintype α] (f : α β) :
theorem fintype.card_congr {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) :
theorem fintype.card_congr' {α β : Type u_1} [fintype α] [fintype β] (h : α = β) :
def fintype.trunc_equiv_fin_of_card_eq {α : Type u_1} [fintype α] [decidable_eq α] {n : } (h : fintype.card α = n) :
trunc fin n)

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
noncomputable def fintype.equiv_fin_of_card_eq {α : Type u_1} [fintype α] {n : } (h : fintype.card α = n) :
α fin n

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
def fintype.trunc_equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] (h : fintype.card α = fintype.card β) :
trunc β)

Two fintypes 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
noncomputable def fintype.equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : fintype.card α = fintype.card β) :
α β

Two fintypes 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
theorem fintype.card_eq {α : Type u_1} {β : Type u_2} [F : fintype α] [G : fintype β] :
def fintype.of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

Any subsingleton type with a witness is a fintype (with one term).

Equations
@[simp]
theorem fintype.univ_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :
@[simp]
theorem fintype.card_of_subsingleton {α : Type u_1} (a : α) [subsingleton α] :

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.

@[simp]
theorem fintype.card_unique {α : Type u_1} [unique α] [h : fintype α] :
@[protected, instance]
def fintype.of_is_empty {α : Type u_1} [is_empty α] :
Equations
@[simp, nolint]
theorem fintype.univ_of_is_empty {α : Type u_1} [is_empty α] :

Note: this lemma is specifically about fintype.of_is_empty. For a statement about arbitrary fintype instances, use finset.univ_eq_empty.

@[simp]
theorem fintype.card_of_is_empty {α : Type u_1} [is_empty α] :

Note: this lemma is specifically about fintype.of_is_empty. For a statement about arbitrary fintype instances, use fintype.card_eq_zero_iff.

def set.to_finset {α : Type u_1} (s : set α) [fintype s] :

Construct a finset enumerating a set s, given a fintype instance.

Equations
theorem set.to_finset_congr {α : Type u_1} {s t : set α} [fintype s] [fintype t] (h : s = t) :
@[simp]
theorem set.mem_to_finset {α : Type u_1} {s : set α} [fintype s] {a : α} :
@[simp]
theorem set.mem_to_finset_val {α : Type u_1} {s : set α} [fintype s] {a : α} :
def set.decidable_mem_of_fintype {α : Type u_1} [decidable_eq α] (s : set α) [fintype s] (a : α) :

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
@[simp]
theorem set.to_finset_card {α : Type u_1} (s : set α) [fintype s] :
@[simp]
theorem set.coe_to_finset {α : Type u_1} (s : set α) [fintype s] :
@[simp]
theorem set.to_finset_inj {α : Type u_1} {s t : set α} [fintype s] [fintype t] :
@[simp]
theorem set.to_finset_subset {α : Type u_1} {s t : set α} [fintype s] [fintype t] :
@[simp]
theorem set.to_finset_ssubset {α : Type u_1} {s t : set α} [fintype s] [fintype t] :
@[simp]
theorem set.to_finset_disjoint_iff {α : Type u_1} [decidable_eq α] {s t : set α} [fintype s] [fintype t] :
theorem set.to_finset_inter {α : Type u_1} [decidable_eq α] (s t : set α) [fintype (s t)] [fintype s] [fintype t] :
theorem set.to_finset_union {α : Type u_1} [decidable_eq α] (s t : set α) [fintype (s t)] [fintype s] [fintype t] :
theorem set.to_finset_diff {α : Type u_1} [decidable_eq α] (s t : set α) [fintype s] [fintype t] [fintype (s \ t)] :
theorem set.to_finset_ne_eq_erase {α : Type u_1} [decidable_eq α] [fintype α] (a : α) [fintype {x : α | x a}] :
{x : α | x a}.to_finset = finset.univ.erase a
theorem set.to_finset_compl {α : Type u_1} [decidable_eq α] [fintype α] (s : set α) [fintype s] [fintype s] :
@[simp]
@[simp]
theorem set.to_finset_range {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype β] (f : β → α) [fintype (set.range f)] :
theorem set.to_finset_singleton {α : Type u_1} (a : α) [fintype {a}] :
{a}.to_finset = {a}
@[simp]
theorem set.to_finset_insert {α : Type u_1} [decidable_eq α] {a : α} {s : set α} [fintype (has_insert.insert a s)] [fintype s] :
theorem set.filter_mem_univ_eq_to_finset {α : Type u_1} [fintype α] (s : set α) [fintype s] [decidable_pred (λ (_x : α), _x s)] :
finset.filter (λ (_x : α), _x s) finset.univ = s.to_finset
@[simp]
theorem finset.to_finset_coe {α : Type u_1} (s : finset α) [fintype s] :
theorem finset.card_univ {α : Type u_1} [fintype α] :
theorem finset.eq_univ_of_card {α : Type u_1} [fintype α] (s : finset α) (hs : s.card = fintype.card α) :
theorem finset.card_eq_iff_eq_univ {α : Type u_1} [fintype α] (s : finset α) :
theorem finset.card_le_univ {α : Type u_1} [fintype α] (s : finset α) :
theorem finset.card_lt_univ_of_not_mem {α : Type u_1} [fintype α] {s : finset α} {x : α} (hx : x s) :
theorem finset.card_lt_iff_ne_univ {α : Type u_1} [fintype α] (s : finset α) :
theorem finset.card_compl_lt_iff_nonempty {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
theorem finset.card_univ_diff {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :
theorem finset.card_compl {α : Type u_1} [decidable_eq α] [fintype α] (s : finset α) :
@[protected, instance]
def fin.fintype (n : ) :
Equations
theorem fin.univ_def (n : ) :
@[simp]
theorem fintype.card_fin (n : ) :
@[simp]
theorem finset.card_fin (n : ) :

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.

theorem fin.cast_eq_cast' {n m : } (h : fin n = fin m) :

A reversed version of fin.cast_eq_cast that is easier to rewrite with.

theorem card_finset_fin_le {n : } (s : finset (fin n)) :
s.card n
theorem fin.equiv_iff_eq {m n : } :
nonempty (fin m fin n) m = n
@[simp]

Embed fin n into fin (n + 1) by prepending zero to the univ

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

@[instance]
def unique.fintype {α : Type u_1} [unique α] :
Equations
@[protected, instance]
def fintype.subtype_eq {α : Type u_1} (y : α) :
fintype {x // x = y}

Short-circuit instance to decrease search for unique.fintype, since that relies on a subsingleton elimination for unique.

Equations
@[protected, instance]
def fintype.subtype_eq' {α : Type u_1} (y : α) :
fintype {x // y = x}

Short-circuit instance to decrease search for unique.fintype, since that relies on a subsingleton elimination for unique.

Equations
@[simp]
theorem fintype.card_subtype_eq {α : Type u_1} (y : α) [fintype {x // x = y}] :
fintype.card {x // x = y} = 1
@[simp]
theorem fintype.card_subtype_eq' {α : Type u_1} (y : α) [fintype {x // y = x}] :
fintype.card {x // y = x} = 1
@[simp]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem fintype.univ_punit  :
finset.univ = {punit.star}
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem units_int.univ  :
finset.univ = {1, -1}
@[protected, instance]
def additive.fintype {α : Type u_1} [fintype α] :
Equations
@[protected, instance]
def multiplicative.fintype {α : Type u_1} [fintype α] :
Equations
@[simp]
@[protected, instance]
def option.fintype {α : Type u_1} [fintype α] :
Equations
@[simp]
theorem fintype.card_option {α : Type u_1} [fintype α] :
def fintype_of_option {α : Type u_1} [fintype (option α)] :

If option α is a fintype then so is α

Equations
def fintype_of_option_equiv {α : Type u_1} {β : Type u_2} [fintype α] (f : α option β) :

A type is a fintype if its successor (using option) is a fintype.

Equations
@[protected, instance]
def sigma.fintype {α : Type u_1} (β : α → Type u_2) [fintype α] [Π (a : α), fintype (β a)] :
Equations
@[simp]
theorem finset.univ_sigma_univ {α : Type u_1} {β : α → Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
@[protected, instance]
def prod.fintype (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
fintype × β)
Equations
@[simp]
theorem finset.univ_product_univ {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
@[simp]
theorem fintype.card_prod (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
def fintype.prod_left {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype × β)] [nonempty β] :

Given that α × β is a fintype, α is also a fintype.

Equations
def fintype.prod_right {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype × β)] [nonempty α] :

Given that α × β is a fintype, β is also a fintype.

Equations
@[protected, instance]
def ulift.fintype (α : Type u_1) [fintype α] :
Equations
@[simp]
theorem fintype.card_ulift (α : Type u_1) [fintype α] :
@[protected, instance]
def plift.fintype (α : Type u_1) [fintype α] :
Equations
@[simp]
theorem fintype.card_plift (α : Type u_1) [fintype α] :
@[protected, instance]
def order_dual.fintype (α : Type u_1) [fintype α] :
Equations
@[protected, instance]
def order_dual.finite (α : Type u_1) [finite α] :
@[simp]
theorem fintype.card_order_dual (α : Type u_1) [fintype α] :
@[protected, instance]
def lex.fintype (α : Type u_1) [fintype α] :
Equations
@[simp]
theorem fintype.card_lex (α : Type u_1) [fintype α] :
@[protected, instance]
def sum.fintype (α : Type u) (β : Type v) [fintype α] [fintype β] :
fintype β)
Equations
noncomputable def fintype.sum_left {α : Type u_1} {β : Type u_2} [fintype β)] :

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.

Equations
noncomputable def fintype.sum_right {α : Type u_1} {β : Type u_2} [fintype β)] :

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.

Equations
@[simp]
theorem fintype.card_sum {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
def fintype_of_fintype_ne {α : Type u_1} (a : α) (h : fintype {b // b a}) :

If the subtype of all-but-one elements is a fintype then the type itself is a fintype.

Equations

fintype (s : finset α) #

@[protected, instance]
def finset.fintype_coe_sort {α : Type u} (s : finset α) :
Equations
@[simp]
theorem finset.univ_eq_attach {α : Type u} (s : finset α) :

Relation to finite #

In this section we prove that α : Type* is finite if and only if fintype α is nonempty.

@[protected, nolint]
theorem fintype.finite {α : Type u_1} (h : fintype α) :
@[protected, nolint, instance]
def finite.of_fintype (α : Type u_1) [fintype α] :

For efficiency reasons, we want finite instances to have higher priority than ones coming from fintype instances.

theorem finite_iff_nonempty_fintype (α : Type u_1) :
theorem nonempty_fintype (α : Type u_1) [finite α] :
noncomputable def fintype.of_finite (α : Type u_1) [finite α] :

Noncomputably get a fintype instance from a finite instance. This is not an instance because we want fintype instances to be useful for computations.

Equations
theorem finite.of_injective {α : Sort u_1} {β : Sort u_2} [finite β] (f : α → β) (H : function.injective f) :
theorem finite.of_surjective {α : Sort u_1} {β : Sort u_2} [finite α] (f : α → β) (H : function.surjective f) :
theorem finite.exists_max {α : Type u_1} {β : Type u_2} [finite α] [nonempty α] [linear_order β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x f x₀
theorem finite.exists_min {α : Type u_1} {β : Type u_2} [finite α] [nonempty α] [linear_order β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x₀ f x
theorem finite.exists_univ_list (α : Type u_1) [finite α] :
∃ (l : list α), l.nodup ∀ (x : α), x l
theorem fintype.card_le_of_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (hf : function.injective f) :
theorem fintype.card_le_of_embedding {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α β) :
theorem fintype.card_lt_of_injective_of_not_mem {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.injective f) {b : β} (w : b set.range f) :
theorem fintype.card_lt_of_injective_not_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.injective f) (h' : ¬function.surjective f) :
theorem fintype.card_le_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.surjective f) :
theorem fintype.card_range_le {α : Type u_1} {β : Type u_2} (f : α → β) [fintype α] [fintype (set.range f)] :
theorem fintype.card_range {α : Type u_1} {β : Type u_2} {F : Type u_3} [embedding_like F α β] (f : F) [fintype α] [fintype (set.range f)] :
theorem fintype.exists_ne_map_eq_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : fintype.card β < fintype.card α) :
∃ (x y : α), x y f x = f y

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.

theorem fintype.card_eq_one_iff {α : Type u_1} [fintype α] :
fintype.card α = 1 ∃ (x : α), ∀ (y : α), y = x
theorem fintype.card_eq_zero_iff {α : Type u_1} [fintype α] :
theorem fintype.card_eq_zero {α : Type u_1} [fintype α] [is_empty α] :
theorem fintype.card_pos_iff {α : Type u_1} [fintype α] :
theorem fintype.card_pos {α : Type u_1} [fintype α] [h : nonempty α] :
theorem fintype.card_ne_zero {α : Type u_1} [fintype α] [nonempty α] :
theorem fintype.card_le_one_iff {α : Type u_1} [fintype α] :
fintype.card α 1 ∀ (a b : α), a = b
theorem fintype.exists_ne_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < fintype.card α) (a : α) :
∃ (b : α), b a
theorem fintype.exists_pair_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < fintype.card α) :
∃ (a b : α), a b
theorem fintype.card_eq_one_of_forall_eq {α : Type u_1} [fintype α] {i : α} (h : ∀ (j : α), j = i) :
theorem fintype.one_lt_card {α : Type u_1} [fintype α] [h : nontrivial α] :
theorem fintype.one_lt_card_iff {α : Type u_1} [fintype α] :
1 < fintype.card α ∃ (a b : α), a b
theorem fintype.two_lt_card_iff {α : Type u_1} [fintype α] :
2 < fintype.card α ∃ (a b c : α), a b a c b c
theorem fintype.card_of_bijective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} (hf : function.bijective f) :
theorem finite.injective_iff_surjective {α : Type u_1} [finite α] {f : α → α} :
theorem finite.injective_iff_bijective {α : Type u_1} [finite α] {f : α → α} :
theorem finite.surjective_iff_bijective {α : Type u_1} [finite α] {f : α → α} :
theorem finite.injective_iff_surjective_of_equiv {α : Type u_1} {β : Type u_2} [finite α] {f : α → β} (e : α β) :
theorem function.injective.bijective_of_finite {α : Type u_1} [finite α] {f : α → α} :

Alias of the forward direction of finite.injective_iff_bijective.

theorem function.surjective.bijective_of_finite {α : Type u_1} [finite α] {f : α → α} :

Alias of the forward direction of finite.surjective_iff_bijective.

theorem function.injective.surjective_of_fintype {α : Type u_1} {β : Type u_2} [finite α] {f : α → β} (e : α β) :

Alias of the forward direction of finite.injective_iff_surjective_of_equiv.

theorem function.surjective.injective_of_fintype {α : Type u_1} {β : Type u_2} [finite α] {f : α → β} (e : α β) :

Alias of the reverse direction of finite.injective_iff_surjective_of_equiv.

theorem fintype.bijective_iff_injective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :
theorem fintype.bijective_iff_surjective_and_card {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) :
theorem function.left_inverse.right_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} {g : β → α} (hfg : function.left_inverse f g) (hcard : fintype.card α fintype.card β) :
theorem function.right_inverse.left_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} {g : β → α} (hfg : function.right_inverse f g) (hcard : fintype.card β fintype.card α) :
def equiv.of_left_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : fintype.card β fintype.card α) (f : α → β) (g : β → α) (h : function.left_inverse g f) :
α β

Construct an equivalence from functions that are inverse to each other.

Equations
@[simp]
theorem equiv.of_left_inverse_of_card_le_symm_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : fintype.card β fintype.card α) (f : α → β) (g : β → α) (h : function.left_inverse g f) (ᾰ : β) :
((equiv.of_left_inverse_of_card_le hβα f g h).symm) = g ᾰ
@[simp]
theorem equiv.of_left_inverse_of_card_le_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hβα : fintype.card β fintype.card α) (f : α → β) (g : β → α) (h : function.left_inverse g f) (ᾰ : α) :
(equiv.of_left_inverse_of_card_le hβα f g h) = f ᾰ
def equiv.of_right_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : fintype.card α fintype.card β) (f : α → β) (g : β → α) (h : function.right_inverse g f) :
α β

Construct an equivalence from functions that are inverse to each other.

Equations
@[simp]
theorem equiv.of_right_inverse_of_card_le_symm_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : fintype.card α fintype.card β) (f : α → β) (g : β → α) (h : function.right_inverse g f) (ᾰ : β) :
((equiv.of_right_inverse_of_card_le hαβ f g h).symm) = g ᾰ
@[simp]
theorem equiv.of_right_inverse_of_card_le_apply {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hαβ : fintype.card α fintype.card β) (f : α → β) (g : β → α) (h : function.right_inverse g f) (ᾰ : α) :
(equiv.of_right_inverse_of_card_le hαβ f g h) = f ᾰ
theorem fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} :
@[protected, instance]
def list.subtype.fintype {α : Type u_1} [decidable_eq α] (l : list α) :
fintype {x // x l}
Equations
@[protected, instance]
def multiset.subtype.fintype {α : Type u_1} [decidable_eq α] (s : multiset α) :
fintype {x // x s}
Equations
@[protected, instance]
def finset.subtype.fintype {α : Type u_1} (s : finset α) :
fintype {x // x s}
Equations
@[protected, instance]
def finset_coe.fintype {α : Type u_1} (s : finset α) :
Equations
@[simp]
theorem fintype.card_coe {α : Type u_1} (s : finset α) [fintype s] :
noncomputable def finset.equiv_fin {α : Type u_1} (s : finset α) :

Noncomputable equivalence between a finset s coerced to a type and fin s.card.

Equations
noncomputable def finset.equiv_fin_of_card_eq {α : Type u_1} {s : finset α} {n : } (h : s.card = n) :

Noncomputable equivalence between a finset s as a fintype and fin n, when there is a proof that s.card = n.

Equations
noncomputable def finset.equiv_of_card_eq {α : Type u_1} {s t : finset α} (h : s.card = t.card) :

Noncomputable equivalence between two finsets s and t as fintypes when there is a proof that s.card = t.card.

Equations
theorem finset.attach_eq_univ {α : Type u_1} {s : finset α} :
@[protected, instance]
def plift.fintype_Prop (p : Prop) [decidable p] :
Equations
@[protected, instance]
def Prop.fintype  :
fintype Prop
Equations
@[simp]
theorem fintype.card_Prop  :
@[protected, instance]
def subtype.fintype {α : Type u_1} (p : α → Prop) [decidable_pred p] [fintype α] :
fintype {x // p x}
Equations
@[simp]
theorem set.to_finset_eq_empty_iff {α : Type u_1} {s : set α} [fintype s] :
@[simp]
theorem set.to_finset_empty {α : Type u_1} :
def set_fintype {α : Type u_1} [fintype α] (s : set α) [decidable_pred (λ (_x : α), _x s)] :

A set on a fintype, when coerced to a type, is a fintype.

Equations
theorem set_fintype_card_le_univ {α : Type u_1} [fintype α] (s : set α) [fintype s] :
theorem set_fintype_card_eq_univ_iff {α : Type u_1} [fintype α] (s : set α) [fintype s] :
@[simp]
theorem coe_units_equiv_prod_subtype_symm_apply (α : Type u_1) [monoid α] (p : {p // p.fst * p.snd = 1 p.snd * p.fst = 1}) :
@[simp]
theorem units_equiv_prod_subtype_apply_coe (α : Type u_1) [monoid α] (u : αˣ) :
@[simp]
theorem coe_inv_units_equiv_prod_subtype_symm_apply (α : Type u_1) [monoid α] (p : {p // p.fst * p.snd = 1 p.snd * p.fst = 1}) :
def units_equiv_prod_subtype (α : Type u_1) [monoid α] :
αˣ {p // p.fst * p.snd = 1 p.snd * p.fst = 1}

The αˣ type is equivalent to a subtype of α × α.

Equations
@[simp]
theorem units_equiv_ne_zero_apply_coe (α : Type u_1) [group_with_zero α] (a : αˣ) :
def units_equiv_ne_zero (α : Type u_1) [group_with_zero α] :
αˣ {a // a 0}

In a group_with_zero α, the unit group αˣ is equivalent to the subtype of nonzero elements.

Equations
@[simp]
theorem units_equiv_ne_zero_symm_apply (α : Type u_1) [group_with_zero α] (a : {a // a 0}) :
@[protected, instance]
def units.fintype {α : Type u_1} [monoid α] [fintype α] [decidable_eq α] :
Equations
@[protected, instance]
def units.finite {α : Type u_1} [monoid α] [finite α] :
theorem fintype.card_units {α : Type u_1} [group_with_zero α] [fintype α] [fintype αˣ] :
noncomputable def function.embedding.equiv_of_fintype_self_embedding {α : Type u_1} [finite α] (e : α α) :
α α

An embedding from a fintype to itself can be promoted to an equivalence.

Equations
@[simp]
theorem function.embedding.is_empty_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : fintype.card β < fintype.card α) :
is_empty β)

If ‖β‖ < ‖α‖ there are no embeddings α ↪ β. This is a formulation of the pigeonhole principle.

Note this cannot be an instance as it needs h.

def function.embedding.trunc_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] (h : fintype.card α fintype.card β) :
trunc β)

A constructive embedding of a fintype α in another fintype β when card α ≤ card β.

Equations
theorem function.embedding.nonempty_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : fintype.card α fintype.card β) :
nonempty β)
theorem function.embedding.exists_of_card_le_finset {α : Type u_1} {β : Type u_2} [fintype α] {s : finset β} (h : fintype.card α s.card) :
∃ (f : α β), set.range f s
@[simp]
theorem finset.univ_map_embedding {α : Type u_1} [fintype α] (e : α α) :
noncomputable def fintype.finset_equiv_set {α : Type u_1} [fintype α] :
finset α set α

Given fintype α, finset_equiv_set is the equiv between finset α and set α. (All sets on a finite type are finite.)

Equations
@[simp]
theorem fintype.finset_equiv_set_apply {α : Type u_1} [fintype α] (s : finset α) :
@[simp]
theorem fintype.card_lt_of_surjective_not_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.surjective f) (h' : ¬function.injective f) :
def fintype.pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (t : Π (a : α), finset (δ a)) :
finset (Π (a : α), δ a)

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
@[simp]
theorem fintype.mem_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a} :
f fintype.pi_finset t ∀ (a : α), f a t a
@[simp]
theorem fintype.coe_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (t : Π (a : α), finset (δ a)) :
(fintype.pi_finset t) = set.univ.pi (λ (a : α), (t a))
theorem fintype.pi_finset_subset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (t₁ t₂ : Π (a : α), finset (δ a)) (h : ∀ (a : α), t₁ a t₂ a) :
@[simp]
theorem fintype.pi_finset_empty {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} [nonempty α] :
fintype.pi_finset (λ (_x : α), ) =
@[simp]
theorem fintype.pi_finset_singleton {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} (f : Π (i : α), δ i) :
fintype.pi_finset (λ (i : α), {f i}) = {f}
theorem fintype.pi_finset_subsingleton {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} {f : Π (i : α), finset (δ i)} (hf : ∀ (i : α), (f i).subsingleton) :
theorem fintype.pi_finset_disjoint_of_disjoint {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_4} [Π (a : α), decidable_eq (δ a)] (t₁ t₂ : Π (a : α), finset (δ a)) {a : α} (h : disjoint (t₁ a) (t₂ a)) :

pi #

@[protected, instance]
def pi.fintype {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
fintype (Π (a : α), β a)

A dependent product of fintypes, indexed by a fintype, is a fintype.

Equations
@[simp]
theorem fintype.pi_finset_univ {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
@[protected, instance]
def d_array.fintype {n : } {α : fin nType u_1} [Π (n : fin n), fintype (α n)] :
Equations
@[protected, instance]
def array.fintype {n : } {α : Type u_1} [fintype α] :
fintype (array n α)
Equations
@[protected, instance]
def vector.fintype {α : Type u_1} [fintype α] {n : } :
Equations
@[protected, instance]
def quotient.fintype {α : Type u_1} [fintype α] (s : setoid α) [decidable_rel has_equiv.equiv] :
Equations
@[protected, instance]
def finset.fintype {α : Type u_1} [fintype α] :
Equations
@[protected, instance]
def function.embedding.fintype {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] :
fintype β)
Equations
@[protected, instance]
def sym.sym'.fintype {α : Type u_1} [decidable_eq α] [fintype α] {n : } :
Equations
@[protected, instance]
def sym.fintype {α : Type u_1} [decidable_eq α] [fintype α] {n : } :
fintype (sym α n)
Equations
@[simp]
theorem fintype.card_finset {α : Type u_1} [fintype α] :
@[simp]
theorem finset.powerset_univ {α : Type u_1} [fintype α] :
@[simp]
theorem finset.powerset_eq_univ {α : Type u_1} [fintype α] {s : finset α} :
theorem finset.mem_powerset_len_univ_iff {α : Type u_1} [fintype α] {s : finset α} {k : } :
@[simp]
theorem finset.univ_filter_card_eq (α : Type u_1) [fintype α] (k : ) :
@[simp]
theorem fintype.card_finset_len {α : Type u_1} [fintype α] (k : ) :
theorem fintype.card_subtype_le {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
theorem fintype.card_subtype_lt {α : Type u_1} [fintype α] {p : α → Prop} [decidable_pred p] {x : α} (hx : ¬p x) :
theorem fintype.card_subtype {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] :
theorem fintype.card_subtype_or {α : Type u_1} (p q : α → Prop) [fintype {x // p x}] [fintype {x // q x}] [fintype {x // p x q x}] :
fintype.card {x // p x q x} fintype.card {x // p x} + fintype.card {x // q x}
theorem fintype.card_subtype_or_disjoint {α : Type u_1} (p q : α → Prop) (h : disjoint p q) [fintype {x // p x}] [fintype {x // q x}] [fintype {x // p x q x}] :
fintype.card {x // p x q x} = fintype.card {x // p x} + fintype.card {x // q x}
@[simp]
theorem fintype.card_subtype_compl {α : Type u_1} [fintype α] (p : α → Prop) [fintype {x // p x}] [fintype {x // ¬p x}] :
fintype.card {x // ¬p x} = fintype.card α - fintype.card {x // p x}
theorem fintype.card_subtype_mono {α : Type u_1} (p q : α → Prop) (h : p q) [fintype {x // p x}] [fintype {x // q x}] :
fintype.card {x // p x} fintype.card {x // q x}
theorem fintype.card_compl_eq_card_compl {α : Type u_1} [finite α] (p q : α → Prop) [fintype {x // p x}] [fintype {x // ¬p x}] [fintype {x // q x}] [fintype {x // ¬q x}] (h : fintype.card {x // p x} = fintype.card {x // q x}) :
fintype.card {x // ¬p x} = fintype.card {x // ¬q x}

If two subtypes of a fintype have equal cardinality, so do their complements.

theorem fintype.card_quotient_lt {α : Type u_1} [fintype α] {s : setoid α} [decidable_rel has_equiv.equiv] {x y : α} (h1 : x y) (h2 : x y) :
@[protected, instance]
def psigma.fintype {α : Type u_1} {β : α → Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations
@[protected, instance]
def psigma.fintype_prop_left {α : Prop} {β : α → Type u_1} [decidable α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations
@[protected, instance]
def psigma.fintype_prop_right {α : Type u_1} {β : α → Prop} [Π (a : α), decidable (β a)] [fintype α] :
fintype (Σ' (a : α), β a)
Equations
@[protected, instance]
def psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [Π (a : α), decidable (β a)] :
fintype (Σ' (a : α), β a)
Equations
@[protected, instance]
def set.fintype {α : Type u_1} [fintype α] :
Equations
@[protected, instance]
def set.finite' {α : Type u_1} [finite α] :
finite (set α)
@[simp]
theorem fintype.card_set {α : Type u_1} [fintype α] :
@[protected, instance]
def pfun_fintype (p : Prop) [decidable p] (α : p → Type u_1) [Π (hp : p), fintype (α hp)] :
fintype (Π (hp : p), α hp)
Equations
@[simp]
theorem finset.univ_pi_univ {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
theorem mem_image_univ_iff_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} {b : β} :
def quotient.fin_choice_aux {ι : Type u_1} [decidable_eq ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) :
(Π (i : ι), i lquotient (S i))quotient pi_setoid

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
theorem quotient.fin_choice_aux_eq {ι : Type u_1} [decidable_eq ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) (f : Π (i : ι), i lα i) :
quotient.fin_choice_aux l (λ (i : ι) (h : i l), f i h) = f
def quotient.fin_choice {ι : Type u_1} [decidable_eq ι] [fintype ι] {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (f : Π (i : ι), quotient (S i)) :

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
theorem quotient.fin_choice_eq {ι : Type u_1} [decidable_eq ι] [fintype ι] {α : ι → Type u_2} [Π (i : ι), setoid (α i)] (f : Π (i : ι), α i) :
quotient.fin_choice (λ (i : ι), f i) = f
def perms_of_list {α : Type u_1} [decidable_eq α] :
list αlist (equiv.perm α)

Given a list, produce a list of all permutations of its elements.

Equations
theorem length_perms_of_list {α : Type u_1} [decidable_eq α] (l : list α) :
theorem mem_perms_of_list_of_mem {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} (h : ∀ (x : α), f x xx l) :
theorem mem_of_mem_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
f perms_of_list l∀ {x : α}, f x xx l
theorem mem_perms_of_list_iff {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
f perms_of_list l ∀ {x : α}, f x xx l
theorem nodup_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) :
def perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :

Given a finset, produce the finset of all permutations of its elements.

Equations
theorem mem_perms_of_finset_iff {α : Type u_1} [decidable_eq α] {s : finset α} {f : equiv.perm α} :
f perms_of_finset s ∀ {x : α}, f x xx s
theorem card_perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
def fintype_perm {α : Type u_1} [decidable_eq α] [fintype α] :

The collection of permutations of a fintype is a fintype.

Equations
@[protected, instance]
def equiv.fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
fintype β)
Equations
theorem fintype.card_equiv {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] (e : α β) :
theorem univ_eq_singleton_of_card_one {α : Type u_1} [fintype α] (x : α) (h : fintype.card α = 1) :
def fintype.choose_x {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :
{a // p a}

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
def fintype.choose {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :
α

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
theorem fintype.choose_spec {α : Type u_1} [fintype α] (p : α → Prop) [decidable_pred p] (hp : ∃! (a : α), p a) :
@[simp]
theorem fintype.choose_subtype_eq {α : Type u_1} (p : α → Prop) [fintype {a // p a}] [decidable_eq α] (x : {a // p a}) (h : (∃! (a : {a // p a}), a = x) := _) :
fintype.choose (λ (y : {a // p a}), y = x) h = x
def fintype.bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) (b : β) :
α

bij_inv f is the unique inverse to a bijection f. This acts as a computable alternative to function.inv_fun.

Equations
theorem fintype.left_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
theorem fintype.right_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
theorem fintype.bijective_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
theorem finite.well_founded_of_trans_of_irrefl {α : Type u_1} [finite α] (r : α → α → Prop) [is_trans α r] [is_irrefl α r] :
theorem finite.preorder.well_founded_gt {α : Type u_1} [finite α] [preorder α] :
@[protected, instance]
@[protected, instance]
theorem not_finite (α : Type u_1) [infinite α] [finite α] :
@[protected]
theorem finite.false {α : Type u_1} [infinite α] (h : finite α) :
@[protected, nolint]
theorem fintype.false {α : Type u_1} [infinite α] (h : fintype α) :
@[protected]
theorem infinite.false {α : Type u_1} [finite α] (h : infinite α) :
@[simp]
theorem is_empty_fintype {α : Type u_1} :
theorem not_finite_iff_infinite {α : Type u_1} :
theorem not_infinite_iff_finite {α : Type u_1} :
theorem infinite.of_not_finite {α : Type u_1} :
¬finite αinfinite α

Alias of the forward direction of not_finite_iff_infinite.

theorem infinite.not_finite {α : Type u_1} :
infinite α¬finite α

Alias of the reverse direction of not_finite_iff_infinite.

theorem finite.of_not_infinite {α : Type u_1} :
¬infinite αfinite α

Alias of the forward direction of not_infinite_iff_finite.

theorem finite.not_infinite {α : Type u_1} :
finite α¬infinite α

Alias of the reverse direction of not_infinite_iff_finite.

noncomputable def fintype_of_not_infinite {α : Type u_1} (h : ¬infinite α) :

A non-infinite type is a fintype.

Equations
noncomputable def fintype_or_infinite (α : Type u_1) :

Any type is (classically) either a fintype, or infinite.

One can obtain the relevant typeclasses via cases fintype_or_infinite α; resetI.

Equations
theorem finset.exists_minimal {α : Type u_1} [preorder α] (s : finset α) (h : s.nonempty) :
∃ (m : α) (H : m s), ∀ (x : α), x s¬x < m
theorem finset.exists_maximal {α : Type u_1} [preorder α] (s : finset α) (h : s.nonempty) :
∃ (m : α) (H : m s), ∀ (x : α), x s¬m < x
theorem infinite.exists_not_mem_finset {α : Type u_1} [infinite α] (s : finset α) :
∃ (x : α), x s
@[protected, instance]
def infinite.nontrivial (α : Type u_1) [H : infinite α] :
@[protected]
theorem infinite.nonempty (α : Type u_1) [infinite α] :
theorem infinite.of_injective {α : Type u_1} {β : Type u_2} [infinite β] (f : β → α) (hf : function.injective f) :
theorem infinite.of_surjective {α : Type u_1} {β : Type u_2} [infinite β] (f : α → β) (hf : function.surjective f) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def infinite.set {α : Type u_1} [infinite α] :
@[protected, instance]
def finset.infinite {α : Type u_1} [infinite α] :
@[protected, instance]
def multiset.infinite {α : Type u_1} [nonempty α] :
@[protected, instance]
def list.infinite {α : Type u_1} [nonempty α] :
@[protected, instance]
def option.infinite {α : Type u_1} [infinite α] :
@[protected, instance]
def sum.infinite_of_left {α : Type u_1} {β : Type u_2} [infinite α] :
infinite β)
@[protected, instance]
def sum.infinite_of_right {α : Type u_1} {β : Type u_2} [infinite β] :
infinite β)
@[simp]
theorem infinite_sum {α : Type u_1} {β : Type u_2} :
@[protected, instance]
def prod.infinite_of_right {α : Type u_1} {β : Type u_2} [nonempty α] [infinite β] :
infinite × β)
@[protected, instance]
def prod.infinite_of_left {α : Type u_1} {β : Type u_2} [infinite α] [nonempty β] :
infinite × β)
@[simp]
theorem infinite_prod {α : Type u_1} {β : Type u_2} :
noncomputable def infinite.nat_embedding (α : Type u_1) [infinite α] :
α

Embedding of into an infinite type.

Equations
theorem infinite.exists_subset_card_eq (α : Type u_1) [infinite α] (n : ) :
∃ (s : finset α), s.card = n

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.

theorem infinite.exists_superset_card_eq {α : Type u_1} [infinite α] (s : finset α) (n : ) (hn : s.card n) :
∃ (t : finset α), s t t.card = n

See infinite.exists_subset_card_eq for a version that provides an arbitrary s : finset α for any cardinality.

noncomputable def fintype_of_finset_card_le {ι : Type u_1} (n : ) (w : ∀ (s : finset ι), s.card n) :

If every finset in a type has bounded cardinality, that type is finite.

Equations
theorem not_injective_infinite_finite {α : Type u_1} {β : Type u_2} [infinite α] [finite β] (f : α → β) :
theorem finite.exists_ne_map_eq_of_infinite {α : Type u_1} {β : Type u_2} [infinite α] [finite β] (f : α → β) :
∃ (x y : α), x y f x = f y

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.

@[protected, instance]
def function.embedding.is_empty {α : Type u_1} {β : Type u_2} [infinite α] [finite β] :
is_empty β)
theorem finite.exists_infinite_fiber {α : Type u_1} {β : Type u_2} [infinite α] [finite β] (f : α → β) :
∃ (y : β), infinite (f ⁻¹' {y})

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

theorem not_surjective_finite_infinite {α : Type u_1} {β : Type u_2} [finite α] [infinite β] (f : α → β) :
def trunc_of_multiset_exists_mem {α : Type u_1} (s : multiset α) :
(∃ (x : α), x s)trunc α

For s : multiset α, we can lift the existential statement that ∃ x, x ∈ s to a trunc α.

Equations
def trunc_of_nonempty_fintype (α : Type u_1) [nonempty α] [fintype α] :

A nonempty fintype constructively contains an element.

Equations
def trunc_of_card_pos {α : Type u_1} [fintype α] (h : 0 < fintype.card α) :

A fintype with positive cardinality constructively contains an element.

Equations
def trunc_sigma_of_exists {α : Type u_1} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ (a : α), P a) :
trunc (Σ' (a : α), P a)

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
@[simp]
theorem multiset.count_univ {α : Type u_1} [fintype α] [decidable_eq α] (a : α) :
def fintype.trunc_rec_empty_option {P : Type uSort v} (of_equiv : Π {α β : Type u}, α βP αP β) (h_empty : P pempty) (h_option : Π {α : Type u} [_inst_1 : fintype α] [_inst_2 : decidable_eq α], P αP (option α)) (α : Type u) [fintype α] [decidable_eq α] :
trunc (P α)

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
theorem fintype.induction_empty_option {P : Π (α : Type u) [_inst_1 : fintype α], Prop} (of_equiv : ∀ (α β : Type u) [_inst_2 : fintype β] (e : α β), P αP β) (h_empty : P pempty) (h_option : ∀ (α : Type u) [_inst_3 : fintype α], P αP (option α)) (α : Type u) [fintype α] :
P α

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.

theorem finite.induction_empty_option {P : Type u → Prop} (of_equiv : ∀ {α β : Type u}, α βP αP β) (h_empty : P pempty) (h_option : ∀ {α : Type u} [_inst_1 : fintype α], P αP (option α)) (α : Type u) [finite α] :
P α

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.

noncomputable def seq_of_forall_finset_exists_aux {α : Type u_1} [decidable_eq α] (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : finset α), ∃ (y : α), (∀ (x : α), x sP x)(P y ∀ (x : α), x sr x y)) :
→ α

Auxiliary definition to show exists_seq_of_forall_finset_exists.

Equations
theorem exists_seq_of_forall_finset_exists {α : Type u_1} (P : α → Prop) (r : α → α → Prop) (h : ∀ (s : finset α), (∀ (x : α), x sP x)(∃ (y : α), P y ∀ (x : α), x sr x y)) :
∃ (f : → α), (∀ (n : ), P (f n)) ∀ (m n : ), m < nr (f m) (f n)

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.

theorem exists_seq_of_forall_finset_exists' {α : Type u_1} (P : α → Prop) (r : α → α → Prop) [is_symm α r] (h : ∀ (s : finset α), (∀ (x : α), x sP x)(∃ (y : α), P y ∀ (x : α), x sr x y)) :
∃ (f : → α), (∀ (n : ), P (f n)) ∀ (m n : ), m nr (f m) (f n)

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.

theorem fintype.induction_subsingleton_or_nontrivial {P : Π (α : Type u_1) [_inst_1 : fintype α], Prop} (α : Type u_1) [fintype α] (hbase : ∀ (α : Type u_1) [_inst_3 : fintype α] [_inst_4 : subsingleton α], P α) (hstep : ∀ (α : Type u_1) [_inst_5 : fintype α] [_inst_6 : nontrivial α], (∀ (β : Type u_1) [_inst_7 : fintype β], fintype.card β < fintype.card αP β)P α) :
P α

A custom induction principle for fintypes. The base case is a subsingleton type, and the induction step is for non-trivial types, and one can assume the hypothesis for smaller types (via fintype.card).

The major premise is fintype α, so to use this with the induction tactic you have to give a name to that instance and use that name.