# mathlibdocumentation

data.fintype.basic

# 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 a `finset` 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 to `finset.univ.card`.
• `perms_of_finset s`: The finset of permutations of the finset `s`.
• `fintype.trunc_equiv_fin`: A fintype `α` is computably equivalent to `fin (card α)`. The `trunc`-free, noncomputable version is `fintype.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` iff `m = n`.
• `infinite α`: Typeclass saying that a type is infinite. Defined as `fintype α → false`.
• `not_fintype`: No `fintype` has an `infinite` 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` and `is_empty_of_card_lt`: Finitely many pigeons and pigeonholes. Weak formulation.
• `fintype.exists_ne_map_eq_of_infinite`: Infinitely many pigeons in finitely many pigeonholes. Weak formulation.
• `fintype.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. See `fintype.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. See `fintype.of_injective` and `fintype.of_surjective`.
• Types which have an injection from/a surjection to an `infinite` type are themselves `infinite`. See `infinite.of_injective` and `infinite.of_surjective`.
@[class]
structure fintype (α : Type u_4) :
Type u_4
• elems :
• complete : ∀ (x : α),

`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
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 : α) :
@[simp]
theorem finset.coe_univ {α : Type u_1} [fintype α] :
theorem finset.univ_nonempty_iff {α : Type u_1} [fintype α] :
theorem finset.univ_nonempty {α : Type u_1} [fintype α] [nonempty α] :
theorem finset.univ_eq_empty {α : Type u_1} [fintype α] :
theorem finset.univ_eq_empty' {α : Type u_1} [fintype α] :
@[simp]
theorem finset.subset_univ {α : Type u_1} [fintype α] (s : finset α) :
@[instance]
def finset.order_top {α : Type u_1} [fintype α] :
Equations
@[instance]
def finset.boolean_algebra {α : Type u_1} [fintype α] [decidable_eq α] :
Equations
theorem finset.compl_eq_univ_sdiff {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
s =
@[simp]
theorem finset.mem_compl {α : Type u_1} [fintype α] [decidable_eq α] {s : finset α} {x : α} :
x s x s
@[simp]
theorem finset.coe_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.union_compl {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.compl_filter {α : Type u_1} [fintype α] [decidable_eq α] (p : α → Prop) [Π (x : α), decidable (¬p x)] :
= finset.filter (λ (x : α), ¬p x) finset.univ
theorem finset.eq_univ_iff_forall {α : Type u_1} [fintype α] {s : finset α} :
∀ (x : α), x s
theorem finset.compl_ne_univ_iff_nonempty {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
@[simp]
theorem finset.univ_inter {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
= s
@[simp]
theorem finset.inter_univ {α : Type u_1} [fintype α] [decidable_eq α] (s : finset α) :
= s
@[simp]
theorem finset.piecewise_univ {α : Type u_1} [fintype α] [Π (i : α), ] {δ : α → Sort u_2} (f g : Π (i : α), δ i) :
= f
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) :
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 =
theorem finset.univ_filter_mem_range {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) [fintype β] [decidable_pred (λ (y : β), y ] [decidable_eq β] :
finset.filter (λ (y : β), y finset.univ =

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

theorem finset.sup_univ_eq_supr {α : Type u_1} {β : Type u_2} [fintype α] (f : α → β) :
= supr 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 α] (f : α → β) :
= infi f

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

@[instance]
def fintype.decidable_pi_fintype {α : Type u_1} {β : α → Type u_2} [Π (a : α), decidable_eq (β a)] [fintype α] :
decidable_eq (Π (a : α), β a)
Equations
@[instance]
def fintype.decidable_forall_fintype {α : Type u_1} {p : α → Prop} [fintype α] :
decidable (∀ (a : α), p a)
Equations
@[instance]
def fintype.decidable_exists_fintype {α : Type u_1} {p : α → Prop} [fintype α] :
decidable (∃ (a : α), p a)
Equations
@[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
@[instance]
def fintype.decidable_eq_equiv_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :
Equations
@[instance]
def fintype.decidable_eq_embedding_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] :
Equations
@[instance]
def fintype.decidable_eq_one_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_one α] [has_one β] :
Equations
@[instance]
def fintype.decidable_eq_zero_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_zero α] [has_zero β] :
@[instance]
def fintype.decidable_eq_mul_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_mul α] [has_mul β] :
Equations
@[instance]
def fintype.decidable_eq_add_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [has_add α] [has_add β] :
@[instance]
def fintype.decidable_eq_add_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α]  :
@[instance]
def fintype.decidable_eq_monoid_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α]  :
Equations
@[instance]
def fintype.decidable_eq_monoid_with_zero_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α]  :
Equations
@[instance]
def fintype.decidable_eq_ring_hom_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [semiring α] [semiring β] :
Equations
@[instance]
def fintype.decidable_injective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] :
Equations
@[instance]
def fintype.decidable_surjective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype α] [fintype β] :
Equations
@[instance]
def fintype.decidable_bijective_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
Equations
@[instance]
def fintype.decidable_right_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] (f : α → β) (g : β → α) :
Equations
@[instance]
def fintype.decidable_left_inverse_fintype {α : Type u_1} {β : Type u_2} [decidable_eq β] [fintype β] (f : α → β) (g : β → α) :
Equations
theorem fintype.exists_max {α : Type u_1} [fintype α] [nonempty α] {β : Type u_2} [linear_order β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x f x₀
theorem fintype.exists_min {α : Type u_1} [fintype α] [nonempty α] {β : Type u_2} [linear_order β] (f : α → β) :
∃ (x₀ : α), ∀ (x : α), f x₀ f x
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
theorem fintype.exists_univ_list (α : Type u_1) [fintype α] :
∃ (l : list α), l.nodup ∀ (x : α), x l
def fintype.card (α : Type u_1) [fintype α] :

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

Equations
def fintype.equiv_fin_of_forall_mem_list {α : Type u_1} [decidable_eq α] {l : list α} (h : ∀ (x : α), x l) (nd : l.nodup) :
α

If `l` lists all the elements of `α` without duplicates, then `α ≃ fin (l.length)`.

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

There is (computably) a bijection between `α` and `fin (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.

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`.

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

There is a (noncomputable) bijection 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
• = let _inst : := in
@[instance]
def fintype.subsingleton (α : Type u_1) :
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 : α β) :
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 : α β) :
def fintype.trunc_equiv_fin_of_card_eq {α : Type u_1} [fintype α] [decidable_eq α] {n : } (h : = 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
def fintype.equiv_fin_of_card_eq {α : Type u_1} [fintype α] {n : } (h : = 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
• = let _inst : := in
def fintype.trunc_equiv_of_card_eq {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] (h : = ) :
trunc β)

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

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
• = let _inst : := , _inst_3 : := in
theorem fintype.card_eq {α : Type u_1} {β : Type u_2} [F : fintype α] [G : fintype β] :
nonempty β)
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 α] :
@[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 `fintype.univ_is_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`.

@[instance]
def fintype.of_subsingleton' (α : Type u_1) [subsingleton α] :

Any subsingleton type is (noncomputably) a fintype (with zero or one term).

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

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

Equations
@[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 : α} :
@[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] :
s = t
@[simp]
theorem set.to_finset_mono {α : Type u_1} {s t : set α} [fintype s] [fintype t] :
s t
@[simp]
theorem set.to_finset_strict_mono {α : Type u_1} {s t : set α} [fintype s] [fintype t] :
s t
@[simp]
theorem set.to_finset_disjoint_iff {α : Type u_1} [decidable_eq α] {s t : set α} [fintype s] [fintype t] :
t
theorem finset.card_univ {α : Type u_1} [fintype α] :
theorem finset.eq_univ_of_card {α : Type u_1} [fintype α] (s : finset α) (hs : s.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 α) :
@[instance]
def fin.fintype (n : ) :
Equations
theorem fin.univ_def (n : ) :
@[simp]
theorem fintype.card_fin (n : ) :
@[simp]
theorem finset.card_fin (n : ) :
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
theorem fin.univ_succ (n : ) :

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

theorem fin.univ_cast_succ (n : ) :

Embed `fin n` into `fin (n + 1)` by appending a new `fin.last n` to the `univ`

theorem fin.univ_succ_above (n : ) (p : fin (n + 1)) :

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
@[simp]
theorem univ_unique {α : Type u_1} [unique α] [f : fintype α] :
@[simp]
theorem univ_is_empty {α : Type u_1} [is_empty α] [fintype α] :
@[simp]
theorem fintype.univ_empty  :
@[simp]
theorem fintype.card_empty  :
@[simp]
theorem fintype.univ_pempty  :
@[simp]
theorem fintype.card_pempty  :
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem fintype.univ_punit  :
@[simp]
theorem fintype.card_punit  :
@[instance]
Equations
@[simp]
@[instance]
Equations
@[simp]
theorem units_int.univ  :
finset.univ = {1, -1}
@[instance]
def additive.fintype {α : Type u_1} [fintype α] :
Equations
@[instance]
def multiplicative.fintype {α : Type u_1} [fintype α] :
Equations
@[simp]
theorem fintype.card_units_int  :
= 2
@[instance]
def units.fintype {α : Type u_1} [monoid α] [fintype α] :
Equations
@[simp]
theorem fintype.card_bool  :
def finset.insert_none {α : Type u_1} (s : finset α) :

Given a finset on `α`, lift it to being a finset on `option α` using `option.some` and then insert `option.none`.

Equations
@[simp]
theorem finset.mem_insert_none {α : Type u_1} {s : finset α} {o : option α} :
o s.insert_none ∀ (a : α), a oa s
theorem finset.some_mem_insert_none {α : Type u_1} {s : finset α} {a : α} :
@[instance]
def option.fintype {α : Type u_1} [fintype α] :
Equations
@[simp]
theorem fintype.card_option {α : Type u_1} [fintype α] :
=
@[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)] :
@[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 β] :
fintype.card × β) =
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
@[instance]
def ulift.fintype (α : Type u_1) [fintype α] :
Equations
@[simp]
theorem fintype.card_ulift (α : Type u_1) [fintype α] :
theorem univ_sum_type {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [fintype β)] [decidable_eq β)] :
@[instance]
def sum.fintype (α : Type u) (β : Type v) [fintype α] [fintype β] :
fintype β)
Equations
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
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

### `fintype (s : finset α)`#

@[instance]
def finset.fintype_coe_sort {α : Type u} (s : finset α) :
Equations
@[simp]
theorem finset.univ_eq_attach {α : Type u} (s : finset α) :
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 ) :
theorem fintype.card_lt_of_injective_not_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.injective f) (h' : ¬) :
theorem fintype.card_le_of_surjective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.surjective f) :
theorem fintype.exists_ne_map_eq_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : < ) :
∃ (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 α] :
∃ (x : α), ∀ (y : α), y = x
theorem fintype.card_eq_zero_iff {α : Type u_1} [fintype α] :
def fintype.card_eq_zero_equiv_equiv_empty {α : Type u_1} [fintype α] :
empty)

A `fintype` with cardinality zero is equivalent to `empty`.

Equations
theorem fintype.card_pos_iff {α : Type u_1} [fintype α] :
theorem fintype.card_le_one_iff {α : Type u_1} [fintype α] :
∀ (a b : α), a = b
theorem fintype.card_le_one_iff_subsingleton {α : Type u_1} [fintype α] :
theorem fintype.one_lt_card_iff_nontrivial {α : Type u_1} [fintype α] :
theorem fintype.exists_ne_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < ) (a : α) :
∃ (b : α), b a
theorem fintype.exists_pair_of_one_lt_card {α : Type u_1} [fintype α] (h : 1 < ) :
∃ (a b : α), a b
theorem fintype.card_eq_one_of_forall_eq {α : Type u_1} [fintype α] {i : α} (h : ∀ (j : α), j = i) :
theorem fintype.injective_iff_surjective {α : Type u_1} [fintype α] {f : α → α} :
theorem fintype.injective_iff_bijective {α : Type u_1} [fintype α] {f : α → α} :
theorem fintype.surjective_iff_bijective {α : Type u_1} [fintype α] {f : α → α} :
theorem fintype.injective_iff_surjective_of_equiv {α : Type u_1} [fintype α] {β : Type u_2} {f : α → β} (e : α β) :
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 fintype.right_inverse_of_left_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} {g : β → α} (hfg : g) (hcard : ) :
theorem fintype.left_inverse_of_right_inverse_of_card_le {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] {f : α → β} {g : β → α} (hfg : g) (hcard : ) :
theorem fintype.coe_image_univ {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} :
@[instance]
def list.subtype.fintype {α : Type u_1} [decidable_eq α] (l : list α) :
fintype {x // x l}
Equations
@[instance]
def multiset.subtype.fintype {α : Type u_1} [decidable_eq α] (s : multiset α) :
fintype {x // x s}
Equations
@[instance]
def finset.subtype.fintype {α : Type u_1} (s : finset α) :
fintype {x // x s}
Equations
@[instance]
def finset_coe.fintype {α : Type u_1} (s : finset α) :
Equations
@[simp]
theorem fintype.card_coe {α : Type u_1} (s : finset α) :
theorem finset.attach_eq_univ {α : Type u_1} {s : finset α} :
@[instance]
def plift.fintype (p : Prop) [decidable p] :
Equations
@[instance]
def Prop.fintype  :
fintype Prop
Equations
@[instance]
def subtype.fintype {α : Type u_1} (p : α → Prop) [fintype α] :
fintype {x // p x}
Equations
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] :
def function.embedding.equiv_of_fintype_self_embedding {α : Type u_1} [fintype α] (e : α α) :
α α

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

Equations
@[simp]
@[simp]
theorem function.embedding.is_empty_of_card_lt {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (h : < ) :
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`.

@[simp]
theorem finset.univ_map_embedding {α : Type u_1} [fintype α] (e : α α) :
theorem fintype.card_lt_of_surjective_not_injective {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (f : α → β) (h : function.surjective f) (h' : ¬) :
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} :
∀ (a : α), f 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) :
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 #

@[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)] :
@[instance]
def d_array.fintype {n : } {α : fin nType u_1} [Π (n : fin n), fintype (α n)] :
Equations
@[instance]
def array.fintype {n : } {α : Type u_1} [fintype α] :
fintype (array n α)
Equations
@[instance]
def vector.fintype {α : Type u_1} [fintype α] {n : } :
Equations
@[instance]
def quotient.fintype {α : Type u_1} [fintype α] (s : setoid α)  :
Equations
@[instance]
def finset.fintype {α : Type u_1} [fintype α] :
Equations
@[instance]
def function.embedding.fintype {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] :
fintype β)
Equations
@[instance]
def sym.sym'.fintype {α : Type u_1} [decidable_eq α] [fintype α] {n : } :
Equations
@[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.univ_filter_card_eq (α : Type u_1) [fintype α] (k : ) :
finset.filter (λ (s : finset α), s.card = k) finset.univ =
@[simp]
theorem fintype.card_finset_len {α : Type u_1} [fintype α] (k : ) :
@[simp]
theorem set.to_finset_univ {α : Type u_1} [fintype α] :
@[simp]
theorem set.to_finset_eq_empty_iff {α : Type u_1} {s : set α} [fintype s] :
s =
@[simp]
theorem set.to_finset_empty {α : Type u_1} :
@[simp]
theorem set.to_finset_range {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype β] (f : β → α) [fintype (set.range f)] :
theorem fintype.card_subtype_le {α : Type u_1} [fintype α] (p : α → Prop)  :
fintype.card {x // p x}
theorem fintype.card_subtype_lt {α : Type u_1} [fintype α] {p : α → Prop} {x : α} (hx : ¬p x) :
fintype.card {x // p x} <
theorem fintype.card_quotient_le {α : Type u_1} [fintype α] (s : setoid α)  :
theorem fintype.card_quotient_lt {α : Type u_1} [fintype α] {s : setoid α} {x y : α} (h1 : x y) (h2 : x y) :
@[instance]
def psigma.fintype {α : Type u_1} {β : α → Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations
@[instance]
def psigma.fintype_prop_left {α : Prop} {β : α → Type u_1} [decidable α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations
@[instance]
def psigma.fintype_prop_right {α : Type u_1} {β : α → Prop} [Π (a : α), decidable (β a)] [fintype α] :
fintype (Σ' (a : α), β a)
Equations
@[instance]
def psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [Π (a : α), decidable (β a)] :
fintype (Σ' (a : α), β a)
Equations
@[instance]
def set.fintype {α : Type u_1} [fintype α] :
Equations
@[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 : β} :
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))

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) :
(λ (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
• = quotient.lift_on (λ (l : list ι), (λ (i : ι) (_x : i l), f i)) _) (λ (f : Π (i : ι), α i), (λ (i : ι), f i _)) quotient.fin_choice._proof_2
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 α} :
∀ {x : α}, f x xx l
theorem mem_perms_of_list_iff {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
∀ {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 α} :
∀ {x : α}, f x xx s
theorem card_perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
.card = (s.card)!
def fintype_perm {α : Type u_1} [decidable_eq α] [fintype α] :

The collection of permutations of a fintype is a fintype.

Equations
@[instance]
def equiv.fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
fintype β)
Equations
theorem fintype.card_perm {α : Type u_1} [decidable_eq α] [fintype α] :
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 : = 1) :
def fintype.choose_x {α : Type u_1} [fintype α] (p : α → Prop) (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) (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) (hp : ∃! (a : α), p a) :
p hp)
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) :
f
theorem fintype.right_inverse_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
f
theorem fintype.bijective_bij_inv {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] {f : α → β} (f_bij : function.bijective f) :
theorem fintype.well_founded_of_trans_of_irrefl {α : Type u_1} [fintype α] (r : α → α → Prop) [ r] [ r] :
theorem fintype.preorder.well_founded {α : Type u_1} [fintype α] [preorder α] :
@[instance]
theorem fintype.linear_order.is_well_order {α : Type u_1} [fintype α] [linear_order α] :
@[class]
structure infinite (α : Type u_4) :
Prop
• not_fintype : false

A type is said to be infinite if it has no fintype instance. Note that `infinite α` is equivalent to `is_empty (fintype α)`.

Instances
theorem not_fintype (α : Type u_1) [h1 : infinite α] [h2 : fintype α] :
theorem fintype.false {α : Type u_1} [infinite α] (h : fintype α) :
theorem infinite.false {α : Type u_1} [fintype α] (h : infinite α) :
@[simp]
theorem is_empty_fintype {α : Type u_1} :
@[simp]
theorem not_nonempty_fintype {α : Type u_1} :
def fintype_of_not_infinite {α : Type u_1} (h : ¬) :

A non-infinite type is a fintype.

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
@[instance]
def infinite.nontrivial (α : Type u_1) [H : infinite α] :
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) :
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
theorem not_injective_infinite_fintype {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] (f : α → β) :
theorem fintype.exists_ne_map_eq_of_infinite {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] (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`, `fintype.exists_infinite_fiber`.

@[instance]
def function.embedding.is_empty {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] :
is_empty β)
@[instance]
def function.embedding.fintype' {α : Type u_1} {β : Type u_2} [fintype β] :
fintype β)
Equations
theorem fintype.exists_infinite_fiber {α : Type u_1} {β : Type u_2} [infinite α] [fintype β] (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: `fintype.exists_ne_map_eq_of_infinite`

theorem not_surjective_fintype_infinite {α : Type u_1} {β : Type u_2} [fintype α] [infinite β] (f : α → β) :
@[instance]
@[instance]
def trunc_of_multiset_exists_mem {α : Type u_1} (s : multiset α) :
(∃ (x : α), x s)

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

Equations
• = (λ (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_of_multiset_exists_mem._match_1 l h list.nil _x =
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 < ) :

A `fintype` with positive cardinality constructively contains an element.

Equations
• = let _inst : := _ in
def trunc_sigma_of_exists {α : Type u_1} [fintype α] {P : α → Prop} (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 : , 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 → Prop} (of_equiv : ∀ {α β : Type u}, α βP αP β) (h_empty : P pempty) (h_option : ∀ {α : Type u} [_inst_1 : 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`.